opening deleted proof-> lots of error dialogs
rbohrer opened this issue · 0 comments
rbohrer commented
Version: 4.9.8
Reproduce:
- create trivial model like 1=1
- prove it
- go back to models dialog
- delete the model
- press Back button in browser to get back to proof page
Got:
- lots of modal popup error dialogs on top of each other, one example is:
Error executing proofs/user/local/undefined/tactic
Reason: the proof is deleted, so of course there are errors
Proposed fix: single error message saying "this proof no longer exists".
Longer term, I do wonder what's the best way to display multiple error messages. I don't have any better idea, but "lots of modal dialogs on top of each other" definitely has happened before
Priority: lowest. I only encountered this because my mouse has a back button that i press by accident.