Re: [isabelle] New error messages in Isabelle 2013

On Wed, 30 Jan 2013, Lars Noschinski wrote:

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.

When you say "the editing focus" and "directly" it already has a strong bias towards the TTY model. Isabelle/jEdit is moving more and more away from that, as far as it becomes feasible. I am especially interested to see decent Isar proof editing facilities, without the TTY side-conditions.

This does not mean that the Output panel of Isabelle/jEdit will just disappear in the next release. There are applications where you do need free-form output from commands.

There are important special cases though:

  (1) proof development, especially structured proof development

  (2) feedback from ATPs via sledgehammer etc.

Here I can imagine more direct user interface support than the old TTY loop.


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