LSP: Retain the last fail state of an obligation.

tlaplus / tlapm

The TLA Proof Manager

https://proofs.tlapl.us/

BSD 2-Clause "Simplified" License

65 stars 20 forks source link

LSP: Retain the last fail state of an obligation. #107

Closed kape1395 closed 9 months ago

kape1395 commented 10 months ago

This is related to #93.

If some backend fails, the failed proof step is reported to the IDE, listing all the assumptions and with the symbols expanded. But then, when the next backend is attempted, the proof state is reset to "proving" with no details on the step. The details could be retained until the step is proven to make the information visible to the user.

kape1395 commented 9 months ago

This is solved in https://github.com/tlaplus/tlapm/pull/93 and https://github.com/tlaplus/vscode-tlaplus/pull/319. The proof state is always shown for the selected proof step, not only on an error.