Re: [isabelle] New error messages in Isabelle 2013



Am 30.01.2013 14:08, schrieb Makarius:
>> 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'll take this as a wordy "yes, but will take some time".

> 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.

Please keep in mind, that the good ol' TTY approach with only one single
point of focus is not overall obsolete: When dealing with a single
proof, one normally only focuses on the lines one is writing. So if
there will be a reasonable replacement for the output window (i.e.
immediate display of messages), this is fine. But having to use the
mouse to get the information is not (even a hotkey for "get message
under cursor" probably will be cumbersome).

- René

-- 
René Neumann

Institut für Informatik (I7)
Technische Universität München
Boltzmannstr. 3
85748 Garching b. München

Tel: +49-89-289-17232
Office: MI 03.11.055

Attachment: smime.p7s
Description: S/MIME Kryptografische Unterschrift



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