[isabelle-dev] Remaining uses of Proof General?
lammich at in.tum.de
Fri Jun 27 14:07:48 CEST 2014
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
Once I have finished the proof, I am interested in the error and warning
messages, and really appreciate the tooltips on the "squiggly" lines.
More information about the isabelle-dev