# HG changeset patch
# User wenzelm
# Date 1355058321 -3600
# Node ID 8dc05db0bf69ed9d347447226698813f6822ead7
# Parent  68c9a6538c0ec8bd21bd8d6a6dc26010cfe6a41f
always apply transitive_reduction_acyclic in imitation of old graph browser (essential to avoid slow layout and overcrowded display, e.g. class_deps);

diff -r 68c9a6538c0e -r 8dc05db0bf69 src/Tools/Graphview/src/graphview.scala
--- 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))
         }
       }
diff -r 68c9a6538c0e -r 8dc05db0bf69 src/Tools/Graphview/src/mutator.scala
--- 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",
diff -r 68c9a6538c0e -r 8dc05db0bf69 src/Tools/jEdit/src/graphview_dockable.scala
--- 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)