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
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
