[isabelle-dev] Remaining uses of Proof General?

[Makarius]

On Fri, 27 Jun 2014, Peter Lammich wrote:

>>    * Regular messages (writeln, warning, error) also appear in the
>>      "squiggly" rendering of the sources, to be hovered over and inspected
>>      without scrolling *the* Output.  There is in fact no reason to have
>>      just one (or two or three) focal points for certain printed results,
>>      like in TTY / PG.
>>
>>    * Tracing is a different topic -- it was never really sorted out
>>      satisfactorily in the history of PG.  More than 1 year ago, Lars Hupel
>>      made some efforts for modernized tracing in PIDE, but it got seriously
>>      encumbered by PG legacy.  It still needs to be revisited just before
>>      the Isabelle2014, to see if it can be made ready for prime time.
>>
>> I don't see any show-stoppers here.  Just more potential for refinements,
>> when PG is discarded.
>
>
> These hints do not adress the problem! During proving, I want to see the
> goal state in first place, not the errors/warnings/etc. If I have to use
> the mouse and scroll down to the goal state every time I change
> something, this really interrupts the working flow during proof
> development.

We should look at this together at VSL 2014, such that I see how your 
present workflow works.

PG has forced a certain model onto the proof assistant in 1998, and I 
adapted to that faithfully in 1999, without ever understanding the real 
policies.  This caused many problems, and in PIDE there is hardly anything 
about such policies: all messages are appended in some canonical order 
produced by the system.

As I have pointed out in my presentation at TUM last december, I would 
like to see some kind of "Preview" of such document state information 
eventually.  But that is music the future, as Florian Haftmann would say.


 	Makarius