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.


	Makarius





This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.