[isabelle-dev] Remaining uses of Proof General?
makarius at sketis.net
Fri Jun 27 13:58:28 CEST 2014
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
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.
More information about the isabelle-dev