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