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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
