src/Tools/Graphview/graph_file.scala
changeset 59459 985fc55e9f27
parent 59443 5b552b4f63a5
child 59460 3a357fef24e8
--- a/src/Tools/Graphview/graph_file.scala	Wed Jan 28 08:29:08 2015 +0100
+++ b/src/Tools/Graphview/graph_file.scala	Wed Jan 28 19:15:13 2015 +0100
@@ -15,9 +15,9 @@
 
 object Graph_File
 {
-  def write(file: JFile, visualizer: Visualizer)
+  def write(file: JFile, graphview: Graphview)
   {
-    val box = visualizer.bounding_box()
+    val box = graphview.bounding_box()
     val w = box.width.ceil.toInt
     val h = box.height.ceil.toInt
 
@@ -26,7 +26,7 @@
       gfx.setColor(Color.WHITE)
       gfx.fillRect(0, 0, w, h)
       gfx.translate(- box.x, - box.y)
-      visualizer.paint_all_visible(gfx)
+      graphview.paint_all_visible(gfx)
     }
 
     val name = file.getName
@@ -40,9 +40,9 @@
     val model = new Model(graph.transitive_reduction_acyclic)
 
     val the_options = options
-    val visualizer = new Visualizer(model) { def options = the_options }
-    visualizer.update_layout()
+    val graphview = new Graphview(model) { def options = the_options }
+    graphview.update_layout()
 
-    write(file, visualizer)
+    write(file, graphview)
   }
 }