Re: [isabelle] New error messages in Isabelle 2013



On 30.01.2013 13:58, Makarius wrote:
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.

I think Peter's point is that he would not like to work with a version of Isabelle where you cannot see directly what is happening at the editing focus. Some of your comments like

| Output and goal states are not fully obsolete yet, but it is one more
| step to overcome them.

can be interpreted as wanting to remove that way of working.

  -- Lars





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