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.

Sign up for GitHub

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 bottom

Open proof explorer by clicking refs in justifications #99

Open
expln opened this issue Jun 12, 2023 · 3 comments
Open

Open proof explorer by clicking refs in justifications #99

expln opened this issue Jun 12, 2023 · 3 comments
Labels
UI UI related

Comments

@expln
Copy link
Owner

expln commented Jun 12, 2023

Copied from #16 (comment) since this will be implemented separately:

click on the ref (opening a dynamic tab on it) and the step used (jumping to it).
@expln expln added the UI UI related label Jun 12, 2023
@david-a-wheeler david-a-wheeler mentioned this issue Jun 25, 2023
Open
expln pushed a commit that referenced this issue Jul 15, 2023
#99 Open proof explorer by clicking refs in justifications.
a73289b
@expln
Copy link
Owner Author

expln commented Jul 15, 2023

@david-a-wheeler "open an explorer tab by clicking a label in the editor" is implemented on dev. I didn't highlight clickable labels, I only changed the shape of the cursor. I tried to make labels similar to usual hyperlinks, but I didn't like how UI was looking. This means less discoverability, but I think this is not a big issue. Clicking on hypotheses numbers is not implemented yet. It will be later.

expln pushed a commit that referenced this issue Jul 16, 2023
#99 Update the tooltip for justifications: "click on the label to ope…
127ca12 
…n a proof explorer tab".
@expln
Copy link
Owner Author

expln commented Jul 16, 2023

I changed the tooltip for justifications. Now it is saying " (Alt+< left-click >) to change; click on the label to open a proof explorer tab".

@expln
Copy link
Owner Author

expln commented Jul 22, 2023

Clicking on hypotheses numbers remains to be implemented.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
UI UI related
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@expln