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