key icon indicating copy to clipboard operation
key copied to clipboard
verified publisher icon KeYProject

Ask before closing a proof whose branches are "used" in other proofs

Open unp1 opened this issue 1 year ago • 2 comments

Please describe your proposal in a ONE sentence

Removing a proof might unexpectedly reopen branches on other proofs

Underlying problem

Removing a proof that is referred to by other proofs causes branches on the other proofs to be reopened

Usage Scenario

When removing a proof via Cmd + W (Ctrl + W) or "Abandon Proof", we should check whether the proof is referred to by branches of other proofs and provide the option to first "copy" the cached branches to the other proofs.

unp1 avatar May 03 '24 13:05 unp1

While it is still a valid feature request to ask for the user choice individually, I just wanted to mention here that there is actually an option under "Options" -> "Show Settings" -> "Proof Caching" to change the behavior: image The default should be "Copy referenced steps", but it seems that in your case it somehow got changed to "Reopen" ...

WolframPfeifer avatar Aug 01 '24 11:08 WolframPfeifer

  • See ProofCachingSettings
  • Is this just a display error or is the default wrong?

Drodt avatar Jan 17 '25 15:01 Drodt