On Fri, 27 Jun 2014, Peter Lammich wrote:
* 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.
We should look at this together at VSL 2014, such that I see how your
present workflow works.
PG has forced a certain model onto the proof assistant in 1998, and I
adapted to that faithfully in 1999, without ever understanding the real
policies. This caused many problems, and in PIDE there is hardly anything
about such policies: all messages are appended in some canonical order
produced by the system.
As I have pointed out in my presentation at TUM last december, I would
like to see some kind of "Preview" of such document state information
eventually. But that is music the future, as Florian Haftmann would say.
Makarius
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
