[isabelle-dev] Towards the next release

[Lukas Bulwahn]

On 04/12/2012 08:32 PM, Makarius wrote:
> 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?
>
We have discussed internally in more detail how to continue, but have 
not made any progress in the implementation itself.

> 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.)
>
Before Stefan starts yet another implementation, we should make sure 
that the different projects converge.


Lukas