Show Proof window

[Alizter]

Could we add an extra window for the extension to do a Show Proof request?

The idea is that sometimes in a proof environment, one would like to inspect the term being built whilst stepping through the proof, for example when inspecting universe levels. The idea is that we would have an extra window that can be toggled on or off that would just do a Show Proof request where the cursor is. This would allow the user to see the proof being built.

We can already do something similar by moving Show Proof manually through the lines, so this feature would make doing that easier. It shouldn't be enabled by default since some proofs would have an expensive call.

[ejgallego]

Yup, you can do that even without modifying the server. Add a command that issues the goals request with a payload command: "Show Proof.", then you can get the answer and display it as you want.

[Alizter]

OK, I will experiment with it when I have some time.