search

expln / metamath-lamp

Metamath-lamp (Lite Assistant for Metamath Proofs) is a GUI-based proof assistant for creating formal mathematical proofs in Metamath that does not require installation (just run it directly using your web browser).
https://expln.github.io/lamp/latest/index.html
MIT License
13 stars 5 forks source link

Open proof explorer by clicking refs in justifications #99

Open expln opened 1 year ago

expln commented 1 year ago

Copied from https://github.com/expln/metamath-lamp/issues/16#issuecomment-1581448444 since this will be implemented separately:

click on the ref (opening a dynamic tab on it) and the step used (jumping to it).

expln commented 1 year ago

@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 commented 1 year ago

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 commented 1 year ago

Clicking on hypotheses numbers remains to be implemented.