--- 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)
--- 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 */
--- 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 =