Re: [isabelle] New error messages in Isabelle 2013



I would like the output panel to remain, if at all possible. Having to click on something to see the current state is cumbersome, and if I understand your comment, it is only available for errors and not for inspection of an arbitrary intermediate proof state. But that's what I often want to do. Moreover, the pop-up windows are quite small and will typically need resizing.
Larry

On 30 Jan 2013, at 13:08, Makarius <makarius at sketis.net> wrote:

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