# HG changeset patch
# User wenzelm
# Date 1422469519 -3600
# Node ID c7eff4356885074043b910c427f51991ec8474b5
# Parent  6eabc60641a6d44828bc9e6ad5b9dea77cd7860a
tuned signature;

diff -r 6eabc60641a6 -r c7eff4356885 src/Tools/Graphview/graph_file.scala
--- a/src/Tools/Graphview/graph_file.scala	Wed Jan 28 19:23:03 2015 +0100
+++ b/src/Tools/Graphview/graph_file.scala	Wed Jan 28 19:25:19 2015 +0100
@@ -37,10 +37,9 @@
 
   def write(options: Options, file: JFile, graph: Graph_Display.Graph)
   {
-    val model = new Model(graph.transitive_reduction_acyclic)
-
     val the_options = options
-    val graphview = new Graphview(model) { def options = the_options }
+    val graphview =
+      new Graphview(graph.transitive_reduction_acyclic) { def options = the_options }
     graphview.update_layout()
 
     write(file, graphview)
diff -r 6eabc60641a6 -r c7eff4356885 src/Tools/Graphview/graphview.scala
--- a/src/Tools/Graphview/graphview.scala	Wed Jan 28 19:23:03 2015 +0100
+++ b/src/Tools/Graphview/graphview.scala	Wed Jan 28 19:25:19 2015 +0100
@@ -15,13 +15,15 @@
 import javax.swing.JComponent
 
 
-abstract class Graphview(val model: Model)
+abstract class Graphview(full_graph: Graph_Display.Graph)
 {
   graphview =>
 
 
   def options: Options
 
+  val model = new Model(full_graph)
+
 
   /* layout state */
 
diff -r 6eabc60641a6 -r c7eff4356885 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Wed Jan 28 19:23:03 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Wed Jan 28 19:25:19 2015 +0100
@@ -61,8 +61,7 @@
   val graphview =
     graph_result match {
       case Exn.Res(graph) =>
-        val model = new isabelle.graphview.Model(graph)
-        val graphview = new isabelle.graphview.Graphview(model) {
+        val graphview = new isabelle.graphview.Graphview(graph) {
           def options: Options = PIDE.options.value
 
           override def make_tooltip(parent: JComponent, x: Int, y: Int, body: XML.Body): String =