[isabelle-dev] Graph_Display.graphview_reportN resp. subtractive change of print mode

[Makarius]

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