# HG changeset patch
# User wenzelm
# Date 1420496978 -3600
# Node ID 126293918a37ba04f4495ae3a7e6ed02b98f51e2
# Parent  305e79989d48d3ae993f1afbdc96fec0c8e35259
clarified visualizer parameters;
do not show dummies by default;

diff -r 305e79989d48 -r 126293918a37 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 23:05:17 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Mon Jan 05 23:29:38 2015 +0100
@@ -96,7 +96,7 @@
       gfx.fillRect(0, 0, peer.getWidth, peer.getHeight)
       gfx.transform(Transform())
 
-      visualizer.Drawer.paint_all_visible(gfx, true)
+      visualizer.paint_all_visible(gfx)
     }
   }
   private val paint_panel = new Paint_Panel
diff -r 305e79989d48 -r 126293918a37 src/Tools/Graphview/main_panel.scala
--- a/src/Tools/Graphview/main_panel.scala	Mon Jan 05 23:05:17 2015 +0100
+++ b/src/Tools/Graphview/main_panel.scala	Mon Jan 05 23:29:38 2015 +0100
@@ -43,6 +43,10 @@
         selected = visualizer.arrow_heads
         action = Action("Arrow heads") { visualizer.arrow_heads = selected; graph_panel.repaint() }
       },
+      new CheckBox() {
+        selected = visualizer.show_dummies
+        action = Action("Show dummies") { visualizer.show_dummies = selected; graph_panel.repaint() }
+      },
       new Button {
         action = Action("Save image") {
           chooser.showSaveDialog(this) match {
@@ -71,7 +75,7 @@
       gfx.setColor(Color.WHITE)
       gfx.fillRect(0, 0, w, h)
       gfx.translate(- box.x, - box.y)
-      visualizer.Drawer.paint_all_visible(gfx, false)
+      visualizer.paint_all_visible(gfx)
     }
 
     try {
diff -r 305e79989d48 -r 126293918a37 src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Mon Jan 05 23:05:17 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Mon Jan 05 23:29:38 2015 +0100
@@ -72,8 +72,7 @@
 
   object Straight_Edge
   {
-    def paint(gfx: Graphics2D, visualizer: Visualizer,
-      edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
+    def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
     {
       val p = visualizer.Coordinates.get_node(edge._1)
       val q = visualizer.Coordinates.get_node(edge._2)
@@ -89,13 +88,15 @@
       ds.foreach(d => path.lineTo(d.x, d.y))
       path.lineTo(q.x, q.y)
 
-      if (dummies) ds.foreach(Dummy.paint(gfx, visualizer, _))
+      if (visualizer.show_dummies)
+        ds.foreach(Dummy.paint(gfx, visualizer, _))
 
       gfx.setStroke(default_stroke)
       gfx.setColor(visualizer.edge_color(edge))
       gfx.draw(path)
 
-      if (head) Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
+      if (visualizer.arrow_heads)
+        Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
     }
   }
 
@@ -103,8 +104,7 @@
   {
     private val slack = 0.1
 
-    def paint(gfx: Graphics2D, visualizer: Visualizer,
-      edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
+    def paint(gfx: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge)
     {
       val p = visualizer.Coordinates.get_node(edge._1)
       val q = visualizer.Coordinates.get_node(edge._2)
@@ -115,7 +115,7 @@
         visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b)
       }
 
-      if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge, head, dummies)
+      if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge)
       else {
         val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
         path.moveTo(p.x, p.y)
@@ -142,13 +142,15 @@
           q.x - slack * dx2, q.y - slack * dy2,
           q.x, q.y)
 
-        if (dummies) ds.foreach(Dummy.paint(gfx, visualizer, _))
+        if (visualizer.show_dummies)
+          ds.foreach(Dummy.paint(gfx, visualizer, _))
 
         gfx.setStroke(default_stroke)
         gfx.setColor(visualizer.edge_color(edge))
         gfx.draw(path)
 
-        if (head) Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
+        if (visualizer.arrow_heads)
+          Arrow_Head.paint(gfx, path, Shapes.Node.shape(visualizer, edge._2))
       }
     }
   }
diff -r 305e79989d48 -r 126293918a37 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Mon Jan 05 23:05:17 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Mon Jan 05 23:29:38 2015 +0100
@@ -52,7 +52,9 @@
 
   /* rendering parameters */
 
+  // owned by GUI thread
   var arrow_heads = false
+  var show_dummies = false
 
   object Colors
   {
@@ -74,6 +76,14 @@
     }
   }
 
+  def paint_all_visible(gfx: Graphics2D)
+  {
+    gfx.setRenderingHints(Metrics.rendering_hints)
+    for (edge <- visible_graph.edges_iterator)
+      Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge)
+    for (node <- visible_graph.keys_iterator)
+      Shapes.Node.paint(gfx, visualizer, node)
+  }
 
   object Coordinates
   {
@@ -129,22 +139,6 @@
     }
   }
 
-  object Drawer
-  {
-    def apply(gfx: Graphics2D, node: Graph_Display.Node): Unit =
-      if (!node.is_dummy) Shapes.Node.paint(gfx, visualizer, node)
-
-    def apply(gfx: Graphics2D, edge: Graph_Display.Edge, head: Boolean, dummies: Boolean): Unit =
-      Shapes.Cardinal_Spline_Edge.paint(gfx, visualizer, edge, head, dummies)
-
-    def paint_all_visible(gfx: Graphics2D, dummies: Boolean)
-    {
-      gfx.setRenderingHints(Metrics.rendering_hints)
-      visible_graph.edges_iterator.foreach(apply(gfx, _, arrow_heads, dummies))
-      visible_graph.keys_iterator.foreach(apply(gfx, _))
-    }
-  }
-
   object Selection
   {
     // owned by GUI thread