Currently, when you have some command, that outputs some info (like thm or term), this output is for a short moment, if at all, shown in the "Prover output" window. But this vanishes as soon as the prover advances.
So, an idea would be to have an additional window/view that holds those information. Perhaps in some way like "line number: message"
For example:
12: 'a list => 'a list
20: ?P => ?Q => ?P && ?Q
Advantage is: One is able to see the output at all. Additionally, one could see the output of multiple commands at the same time. For example in PG one can only see one output at the same time, so one has to toggle between to terms if one wants to compare them.
Currently, when you have some command, that outputs some info (like
thmorterm), this output is for a short moment, if at all, shown in the "Prover output" window. But this vanishes as soon as the prover advances.So, an idea would be to have an additional window/view that holds those information. Perhaps in some way like "line number: message"
For example:
12: 'a list => 'a list20: ?P => ?Q => ?P && ?QAdvantage is: One is able to see the output at all. Additionally, one could see the output of multiple commands at the same time. For example in PG one can only see one output at the same time, so one has to toggle between to
terms if one wants to compare them.