Re: [isabelle] Message output in Isabelle2014 and Isabelle2015
On Tue, 23 Jun 2015, Dmitriy Traytel wrote:
But this would also mean that one does not see the intermediate goal state if
something goes wrong in the terminal method slot of by.
lemma "P (xs :: 'a list)"
by (induct xs) auto
This is more useful when repairing existing proofs, rather than writing new
On 23.06.2015 15:14, Larry Paulson wrote:
Yes â this might be OK.
> On 23 Jun 2015, at 13:42, Peter Lammich <lammich at in.tum.de> wrote:
> One solution that does not involve too much implementation effort might
> be to not include the goal-state into the error message, and output this
> shorter error message *before* the goal-state.
> While the user is typing, he would see a short error message that he
> could ignore, followed by the goal state.
> When the user is inspecting the (error-)result of the command, he would
> see the error message first. Warnings should still be printed after the
The observation by Dmitriy is correct.
The current printing of goal state errors is the result of various reforms
in the past few years. That relatively new behaviour is actually the
reason why I usually do many things without ever looking at the Output
window, often having it closed over a long stretch of time: the message
under the red squiggles usually provides the relevant bits to see what is
missing to finish a proof step.
As already explained on earlier instances of the thread, any built-in
policies to reorder messages in output don't work. We've had that in
Proof General, and it converged to a big mess over the decades. In 2007
that actually caused total existence failure between Proof General 3.x and
4.x. Then I introduced "isabelle tty" as temporary workaround; then
"isabelle jedit" a bit later.
On a multi-window GUI there is no point to squeeze everything into a
single linear output. The Query panel already provides a different way to
view a proof state, independently on Output. Such things are relatively
easy to make, and don't require artificial intelligence from the system to
guess what the user wants to see.
This archive was generated by a fusion of
Pipermail (Mailman edition) and