[isabelle-dev] Making Scala Graph_View happy [was: jdk-8u5]

Makarius makarius at sketis.net
Sun Apr 27 19:59:09 CEST 2014

On Sun, 27 Apr 2014, Florian Haftmann wrote:

> For anyone who wants to start serious work here: this is the current
> state of matters with the existing Scala Graph_View sources:
>> $ LC_ALL=C src/Tools/Graphview/lib/Tools/graphview -b
>> src/Tools/Graphview/lib/Tools/graphview: line 93: isabelle_admin_build: command not found
> (this refers to 70371621fdb6)

As usual, Isabelle tools need to be run within the Isabelle settings 
environment, which is provided by the "isabelle" tools wrapper on the 
command line. So the canonical way is "isabelle graphview -b".  What is 
missing nonetheless, is the classpath for that Scala module, which I have 
now provided in 5b6f4655e2f2.  (That arrangement changed a few times in 
the long time of graphview lying around uselessly.)

For Isabelle/jEdit you merely need to enable the print mode "graphview" 
and then use thy_deps, class_deps etc. as usual. More than 1.5 years ago, 
I spent a lot of time to do all this integration work, only to figure out 
later that the tool was not quite finished, despite its long development 

For the historical record, here is also an old mailing list thread: 
which was started by yourself.

What is missing to make the graphview work in practice:

   * Implement the second half of the layout algorithm, which was somehow
     "forgotten": the Rubber-band method.  (Actually the Hasse Diagramm was
     also forgotten, but I implemented that already myself in the
     Isabelle/Scala Graph module.)

   * Throw out non-essential GUI features, which crash a bit too often.
     Instead concentrate on the core functionality to catch up with the
     1996 version.

   * Eliminate odd gimmicks, e.g. mouse wheel for scaling, instead of the
     usual scrolling behaviour.

   * Provide some way to write out the Graphics2D drawing as PDF.  This
     should be relatively straight-forward using Graphics_File.write_pdf in
     Isabelle/Scala, which I have successfully used already to make the
     parallel performance charts in the ITP-2013 paper.  (The PDF is
     essential for document preparation -- luckily we not longer need PS /

I guess that it would take myself a few days or one week for all that, 
working concentrated just on this thing.  But it is presently unthinkable 
for me to dedicate so much attention to something that is in principle 

In the ancient heroic times, Stefan Berghofer was able to implement the 
whole graph browser from scratch within a 2-3 weeks -- including the 
selection of the layout algorithms from the literature.  His choice is 
still competetive until today, since the only contender -- DOT / Graphviz 
-- did not change much in all these years.


More information about the isabelle-dev mailing list