key icon indicating copy to clipboard operation
key copied to clipboard

Node selection after loading a proof

Open unp1 opened this issue 1 year ago • 4 comments

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.

  1. Save an open proof (with on goal open)
  2. Load the proof
  3. 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

unp1 avatar Oct 13 '23 10:10 unp1