Skip to content
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

👆 Jump-to-definition on click without Ctrl/Cmd in static export #2452

Merged
merged 1 commit into from
Jan 20, 2023

Conversation

fonsp
Copy link
Owner

@fonsp fonsp commented Jan 20, 2023

In a static HTML export, you can now click on underlined global variables to jump to its definition. Before this PR, you had to hold Ctrl/Cmd while clicking. After this PR, Ctrl/Cmd is only required in editing mode. (#2449 would help make this clear.)

Same as #2450, but for HTML instead of PDF. (We can't use the same mechanism because codemirror intercepts the click event and calls .preventDefault(). On the PDF, just using the <a> tag already works, because codemirror is not running when viewing the PDF.)

The tooltip is not changed (Ctrl+Click to jump to the definition of hello_world.), but holding down Ctrl while clicking simply has no effect, so it's still correct 😅

@fonsp fonsp added frontend Concerning the HTML editor online deployment About deploying to binder, heroku, self-hosted wide audience This affects a wide audience of Pluto users and future Pluto users labels Jan 20, 2023
@github-actions
Copy link
Contributor

github-actions bot commented Jan 20, 2023

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="disable-ui-jump-to-definition-without-ctrl")
julia> using Pluto

then open a notebook, and add &disable_ui=true to the URL. (The HTML export file fetches Pluto's JS files from a CDN, so those will not be affected by this PR.)

@fonsp fonsp merged commit e81eeb5 into main Jan 20, 2023
@fonsp fonsp deleted the disable-ui-jump-to-definition-without-ctrl branch January 20, 2023 14:40
fonsp added a commit that referenced this pull request Jan 26, 2023
@fonsp fonsp added the publishing Notebooks as static documents on the web label Oct 30, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
frontend Concerning the HTML editor online deployment About deploying to binder, heroku, self-hosted publishing Notebooks as static documents on the web wide audience This affects a wide audience of Pluto users and future Pluto users
Projects
None yet
Development

Successfully merging this pull request may close these issues.

1 participant