Re: [isabelle] New error messages in Isabelle 2013
On Fri, 25 Jan 2013, Peter Lammich wrote:
When I write proofs, I usually do this
incrementally. If, at some point, I type eg
have foo by auto
and the proof method fails unexpectedly, I would like to immediately see
why, without moving my arm from the keyboard to the mouse, hover the
mouse over the text and wait for the popup.
I am still confused about this confusion. Taking the above specification
in isolation, it is already what happens in Isabelle2013-RC2: you see the
error "immediately" in the output of the by command, assuming that window
is open in the old-fashioned manner; it also works Proof General. If you
don't have output open, then pointing at the red squiggles of "auto" gives
the error more quickly.
If this does not work for you, it might be a remaining problem timing
problem, platform-specific window update problem etc.
This archive was generated by a fusion of
Pipermail (Mailman edition) and