-
Notifications
You must be signed in to change notification settings - Fork 27
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
Node selection after loading a proof #3297
Comments
I agree that selecting an open goal is more useful than selecting the root node. Don't know why it was changed. |
There is an advantage to choose the the root goal initially. On large proofs (highly nested, many nodes), rendering the proof tree takes seconds if you select a nested node. |
Wondering. When saving a proof, we could also store that last selected node (if available) and after loading select this node? So that should be done carefully to not introduce GUI dependencies in ProofSaver |
… selected node in the proof, to reselect it upon loading.
I submitted PR #3324 for discussion. It adds the mentioned feature. |
… selected node in the proof, to reselect it upon loading.
… selected node in the proof, to reselect it upon loading.
… selected node in the proof, to reselect it upon loading.
Description
Loading an open proof selects the root node instead of an open goal.
I am not sure if that may be intended behavior, because one can be of course the
opinion that this is the better way.
In any case, for teaching I sometimes load proofs that have just one branch open and before that branch would be
directly selected, which makes the workflow a bit easier.
In any case, if the change was intended, please close the bug with won't fix.
Reproducible
always
Steps to reproduce
My expectation would be that the open goal is selected.
Additional information
The text was updated successfully, but these errors were encountered: