-
-
Notifications
You must be signed in to change notification settings - Fork 297
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Show hint when you click on a global without Ctrl down #2449
base: main
Are you sure you want to change the base?
Conversation
Try this Pull Request!Open Julia and type: julia> import Pkg
julia> Pkg.activate(temp=true)
julia> Pkg.add(url="https://github.com/fonsp/Pluto.jl", rev="jump-to-definition-tip")
julia> using Pluto |
I agree that it might quickly become too distracting. |
Another stance could be to only show the wiggling underlines (that make the variable a link) |
Thanks for the feedback! This was exactly my thought when I made the underlines bright pink when you press |
🤣 Being so used to the effect, I forgot about it !? |
:) I like the fat underlines, since globals play the lead role in our reactivity. But good to hear your feedback! I will take it into consideration the next time this is up for a restyle. |
I like a lot that globals stand out visually! |
In some recent screen-sharing sessions with Pluto users, I found that the Jump to definition feature is too hidden: people don't know it exists, or they forgot the keyboard shortcut.
This PR will pop up a hint if you click on a global without Ctrl down.
What do people think about this?
See also these two other PRs, which will be merged soon:
Schermopname.2023-01-18.om.18.48.59.mov
TODO:
source_element
, I used the codemirror line element, not just the identifier element. I did this to make the popup show next to the editor, instead of on top of the line. BUT: now you need to click outside the line to hide the popup, clicking somewhere else within the line leaves it open. That does not feel nice.