[isabelle-dev] Remaining uses of Proof General?

[Peter Lammich]

On Fr, 2014-06-27 at 13:58 +0200, Makarius wrote:
> On Fri, 27 Jun 2014, Peter Lammich wrote:
> 
> > * Long list of warnings, e.g. "duplicate simp rule", or tracing messages
> > produced by a method appear before the subgoals in the
> >  output, and thus makes them inaccessible without lots of scrolling.
> > This feature is a real flow-stopper when exploring proofs.
> >
> > In PG, it is possible to have separate buffers for the goal-state, the
> > tracing, and the warning messages, thus you always see the current
> > subgoal you are working on without scrolling down some buffer every
> > time.
> 
> Just a few hints:
> 
>    * 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. 

Once I have finished the proof, I am interested in the error and warning
messages, and really appreciate the tooltips on the "squiggly" lines.

--
  Peter