On Sat, 29 Dec 2012, Florian Haftmann wrote:
The graphview plugin, despite significant progress in the past weeks
esp. wrt. performance, is IMHO still not suitable to manage our typical
graphs (in particular class_deps), mainly due to too small-sized nodes
resp. too wide distances.
Even more is missing to make it approach the quality of the ancient graph
browser by Stefan Berghofer from 1996: it lacks the important "rubberband"
phase to get the layout straight.
The Swing/Scala replacement was added too early to the Isabelle code base,
expecting that it would become better before the release, but it probably
means that I have to finish it myself if nothing happens: removing more of
its experimental features and recovering functionality that was
common-place in the 1996 version.
Unfortunately, the print mode Graph_Display.graphview_reportN is
hardwired from the very beginning of the prover process, and I do not
know about a possibility to do a subtractive patching of the print mode.
Currently I help myself with patching the initialization of the print
mode in ML. Any better suggestions?
You can do it like this while Isabelle/jEdit is running:
ML_command {*
Unsynchronized.change print_mode (remove (op =)
Graph_Display.graphview_reportN)
*}
Makarius
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
