[isabelle-dev] Towards the next release

[Makarius]

On Thu, 12 Apr 2012, Lukas Bulwahn wrote:

> We still have the locale browser in the pipeline. Do you have objections 
> to integrate the tool you have reviewed two months ago? Our private 
> discussion yielded further source code improvements, however the tool is 
> already in a fully functional state, and the source code improvements 
> would not change so much from a user's point of view.

I remember well our discussion with Stefan Berghofer and especially Markus 
Kaiser who did the main work in this project.  We parted at the point 
where everybody observed the little return that JUNG gives for all the 
investment that it requires.  This huge "framework" also seems to be 
unmaintained since 2010, exactly at the moment when I was getting excited 
about it (errornously).

After removing all the initial hopes what JUNG would deliver, only two 
potential benefits were remaining on our list:

   (1) Java object model for graph data structures
   (2) facilities for drawing and a bit of editing of graphs

You had pointed out that a port of the Isabelle graph.ML to Scala would 
make (1) obsolete (which has its own problems due to mutability).  I did 
that in the meantime, and made various refinements so that 
http://isabelle.in.tum.de/repos/isabelle/file/83294cd0e7ee/src/Pure/General/graph.scala 
is pretty stable and closely agrees with the ML version.  I am already 
using graph.scala myself in the Prover IDE document model, to manage 
dependencies of theory buffers etc.

Since (2) is nothing specifically exciting by JUNG either -- it seems to 
be based on plain Java Graphics2D stuff -- I had recommended to abandon 
JUNG altogether. Did anything happen here in the meantime?

I have also spoken to Stefan Berghofer again, and encoraged him to help 
porting his great graph layout tool to Scala.  Conceptually, the old graph 
browser can still compete with newer things on the market, but with its 
use of AWT from Java 1.1 that is hard to explain to end-users. (It is also 
technically hard to integrate into contemporary Swing components.)


 	Makarius