[isabelle-dev] Remaining uses of Proof General?

[Makarius]

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.


 	Makarius