Email Gateway (Aug 19 2022 at 14:15): Email Gateway (Aug 19 2022 at 14:15):From: Florian Haftmann <florian.haftmann@informatik.tu-muenchen.de>
Hi all,
the typical graphs displayed in the graph browser (e.g. as produced by
class_deps after theory Main) are so complex that it is very hard to
find a specific node by name (cf. attached screenshot).
Obviously adding a text search to this ancient AWT application seems out
of focus. But maybe sorting the nodes lexically would be a pragmatic
work-around.
Any opinions?
Cheers,
Florian
class_graph.png
signature.asc
Email Gateway (Aug 19 2022 at 14:15):From: Lawrence Paulson <lp15@cam.ac.uk>
I find them quite tricky to navigate as well. The actual graph doesn’t fit even the largest size and scrolling doesn’t seem to work very well.
Larry
Email Gateway (Aug 19 2022 at 14:15):From: Makarius <makarius@sketis.net>
On Mon, 7 Apr 2014, Florian Haftmann wrote:
Obviously adding a text search to this ancient AWT application seems out
of focus.
That AWT / Java 1.1 graph browser is so ancient that it falls outside of
the usual Isabelle vocabulary of "old", "legacy", "obsolete" etc.
Some years ago there was an initiative to replace it, but the student who
did it spent 2 years on something that turned out to lack half of the
layout algorithm, and was generally unusable.
Since then, the new Graphview is waiting to be finished by someone who
knows a bit of Scala, how the original browser works, and generally how
such things are done properly.
But maybe sorting the nodes lexically would be a pragmatic work-around.
The list is in principle in topological order, but a bit funny due to the
low-level string order that compares length first.
When I introduced the 'class_deps' commands several years ago, it was not
meant very seriously: the class algebra was already beyond naive
browsability at that time.
What I find generally frustrating is that in about 20 years nothing new
seems to have happened concerning DAG layout. People draw funny
undirected "social networks" these days, but still refer to old DOT /
Graphviz for directed graphs.
Makarius
Last updated: Apr 19 2024 at 08:19 UTC