Re: [isabelle] New error messages in Isabelle 2013

On Mon, 28 Jan 2013, René Neumann wrote:

Am 28.01.2013 19:56, schrieb Makarius:

I wouldn't put the output panel in the category of being old-style.
It's a left, right, or bottom dockable window that's part of a modern,
GUI editor. Being able to look at both the edit buffer and the output
panel at the same time at least gives it a dual focus ability.

That is old-school Proof General mode.  When developing complex formal
documents you need more than dual (or triple) focus, but it does not
work by putting more windows there.  One needs to make the one main
window smarter: the source window.

Do I understand this correctly: Eventually, the output panel will
completely be removed and you have to hover the mouse-pointer over
everything to get any information?

I've categorized this as "old-style", "old-fashioned", "old-school". This is one stage before "legacy". After "legacy" comes "discontinued". The full cycle can take many years.

I am still curious to see how far the approach of augmented editing of formal sources can be pushed for Isar proof development, leaving TTY commands and output windows behind. It has been the trajectory of the Prover IDE for several years already, and we are now approaching the point where many technical side-conditions are settled, to make more serious attempts at structured editing support. Isabelle2013 is just one more step, but not the last one.


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