always apply transitive_reduction_acyclic in imitation of old graph browser (essential to avoid slow layout and overcrowded display, e.g. class_deps);
--- a/src/Tools/Graphview/src/graphview.scala Sun Dec 09 14:01:09 2012 +0100
+++ b/src/Tools/Graphview/src/graphview.scala Sun Dec 09 14:05:21 2012 +0100
@@ -30,6 +30,7 @@
args.toList match {
case List(arg) =>
Model.decode_graph(YXML.parse_body(Symbol.decode(File.read(Path.explode(arg)))))
+ .transitive_reduction_acyclic
case _ => error("Bad arguments:\n" + cat_lines(args))
}
}
--- a/src/Tools/Graphview/src/mutator.scala Sun Dec 09 14:01:09 2012 +0100
+++ b/src/Tools/Graphview/src/mutator.scala Sun Dec 09 14:05:21 2012 +0100
@@ -133,7 +133,7 @@
(g, s, d) => !(s == source && d == dest)
)
- case class Edge_Transitive()
+ case class Edge_Transitive() // FIXME slow! / obsolete?!
extends Edge_Filter(
"Hide transitive edges",
--- a/src/Tools/jEdit/src/graphview_dockable.scala Sun Dec 09 14:01:09 2012 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala Sun Dec 09 14:05:21 2012 +0100
@@ -37,12 +37,14 @@
private val graphview = new JPanel
// FIXME mutable GUI content
- private def set_graphview(snapshot: Document.Snapshot, graph: XML.Body)
+ private def set_graphview(snapshot: Document.Snapshot, graph_xml: XML.Body)
{
+ val graph = isabelle.graphview.Model.decode_graph(graph_xml).transitive_reduction_acyclic
+
graphview.removeAll()
graphview.setLayout(new BorderLayout)
val panel =
- new isabelle.graphview.Main_Panel(isabelle.graphview.Model.decode_graph(graph)) {
+ new isabelle.graphview.Main_Panel(graph) {
override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =
{
val rendering = Rendering(snapshot, PIDE.options.value)