key
key copied to clipboard
Node selection after loading a proof
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
Describe the steps needed to reproduce the issue.
- Save an open proof (with on goal open)
- Load the proof
- Root is selected after loading
My expectation would be that the open goal is selected.
Additional information
Add more details here. In particular: if you have a stacktrace, put it here.
- Commit: 05635afb51f8125c62fa9338fdc8f3978ce672a5