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