# HG changeset patch
# User wenzelm
# Date 1421615033 -3600
# Node ID ea163bf8ad22d1b6e9a617ae95b81bbb0751087c
# Parent  fc909f7e7ce51798937c442ea0db902beb229aed
misc tuning;

diff -r fc909f7e7ce5 -r ea163bf8ad22 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Sun Jan 18 21:35:54 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Sun Jan 18 22:03:53 2015 +0100
@@ -22,6 +22,9 @@
 {
   panel =>
 
+
+  /* tooltips */
+
   tooltip = ""
 
   override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
@@ -36,33 +39,32 @@
       }
   }
 
+
+  /* scrolling */
+
   horizontalScrollBarPolicy = ScrollPane.BarPolicy.Always
   verticalScrollBarPolicy = ScrollPane.BarPolicy.Always
 
   peer.getVerticalScrollBar.setUnitIncrement(10)
 
-  def refresh()
+  def scroll_to_node(node: Graph_Display.Node)
   {
-    if (paint_panel != null) {
-      paint_panel.set_preferred_size()
-      paint_panel.repaint()
-    }
+    val gap = visualizer.metrics.gap
+    val info = visualizer.layout.get_node(node)
+
+    val t = Transform()
+    val p =
+      t.transform(new Point2D.Double(info.x - info.width2 - gap, info.y - info.height2 - gap), null)
+    val q =
+      t.transform(new Point2D.Double(info.x + info.width2 + gap, info.y + info.height2 + gap), null)
+
+    paint_panel.peer.scrollRectToVisible(
+      new Rectangle(p.getX.toInt, p.getY.toInt,
+        (q.getX - p.getX).ceil.toInt, (q.getY - p.getY).ceil.toInt))
   }
 
-  def fit_to_window()
-  {
-    Transform.fit_to_window()
-    refresh()
-  }
 
-  val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) }
-
-  def rescale(s: Double)
-  {
-    Transform.scale = s
-    if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).floor.toInt)
-    refresh()
-  }
+  /* painting */
 
   private class Paint_Panel extends Panel
   {
@@ -90,38 +92,33 @@
   private val paint_panel = new Paint_Panel
   contents = paint_panel
 
-  listenTo(mouse.moves)
-  listenTo(mouse.clicks)
-  reactions += Mouse_Interaction.react
-  reactions +=
+  def refresh()
   {
-    case MousePressed(_, _, _, _, _) => repaint()
-    case MouseDragged(_, _, _) => repaint()
-    case MouseClicked(_, _, _, _, _) => repaint()
+    if (paint_panel != null) {
+      paint_panel.set_preferred_size()
+      paint_panel.repaint()
+    }
   }
 
-  visualizer.model.Colors.events += { case _ => repaint() }
-  visualizer.model.Mutators.events += { case _ => repaint() }
+  def fit_to_window()
+  {
+    Transform.fit_to_window()
+    refresh()
+  }
+
+  val zoom = new GUI.Zoom_Box { def changed = rescale(0.01 * factor) }
+
+  def rescale(s: Double)
+  {
+    Transform.scale = s
+    if (zoom != null) zoom.set_item((Transform.scale_discrete * 100).floor.toInt)
+    refresh()
+  }
 
   rescale(1.0)
 
 
-  def scroll_to_node(node: Graph_Display.Node)
-  {
-    val gap = visualizer.metrics.gap
-    val info = visualizer.layout.get_node(node)
-
-    val t = Transform()
-    val p =
-      t.transform(new Point2D.Double(info.x - info.width2 - gap, info.y - info.height2 - gap), null)
-    val q =
-      t.transform(new Point2D.Double(info.x + info.width2 + gap, info.y + info.height2 + gap), null)
-
-    paint_panel.peer.scrollRectToVisible(
-      new Rectangle(p.getX.toInt, p.getY.toInt,
-        (q.getX - p.getX).ceil.toInt, (q.getY - p.getY).ceil.toInt))
-  }
-
+  /* transform */
 
   private object Transform
   {
@@ -166,19 +163,31 @@
     }
   }
 
-  object Mouse_Interaction
-  {
-    private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) = null
+
+  /* interaction */
 
-    val react: PartialFunction[Event, Unit] =
-    {
-      case MousePressed(_, p, _, _, _) => pressed(p)
-      case MouseDragged(_, to, _) =>
-        drag(draginfo, to)
-        val (_, p, d) = draginfo
-        draginfo = (to, p, d)
-      case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e)
-    }
+  listenTo(mouse.moves)
+  listenTo(mouse.clicks)
+  reactions +=
+  {
+    case MousePressed(_, p, _, _, _) =>
+      Mouse_Interaction.pressed(p)
+      repaint()
+    case MouseDragged(_, to, _) =>
+      Mouse_Interaction.dragged(to)
+      repaint()
+    case e @ MouseClicked(_, p, m, n, _) =>
+      Mouse_Interaction.clicked(p, m, n, SwingUtilities.isRightMouseButton(e.peer))
+      repaint()
+  }
+
+  visualizer.model.Colors.events += { case _ => repaint() }
+  visualizer.model.Mutators.events += { case _ => repaint() }
+
+  private object Mouse_Interaction
+  {
+    private var draginfo: (Point, List[Graph_Display.Node], List[Layout.Dummy]) =
+      (new Point(0, 0), Nil, Nil)
 
     def pressed(at: Point)
     {
@@ -198,45 +207,14 @@
       draginfo = (at, l, d)
     }
 
-    def click(at: Point, m: Key.Modifiers, clicks: Int, e: MouseEvent)
+    def dragged(to: Point)
     {
-      val c = Transform.pane_to_graph_coordinates(at)
-
-      def left_click()
-      {
-        (visualizer.find_node(c), m) match {
-          case (Some(node), Key.Modifier.Control) => visualizer.Selection.add(node)
-          case (None, Key.Modifier.Control) =>
-
-          case (Some(node), Key.Modifier.Shift) => visualizer.Selection.add(node)
-          case (None, Key.Modifier.Shift) =>
-
-          case (Some(node), _) =>
-            visualizer.Selection.clear()
-            visualizer.Selection.add(node)
-          case (None, _) =>
-            visualizer.Selection.clear()
-        }
-      }
-
-      def right_click()
-      {
-        val menu = Popups(panel, visualizer.find_node(c), visualizer.Selection.get())
-        menu.show(panel.peer, at.x, at.y)
-      }
-
-      if (clicks < 2) {
-        if (SwingUtilities.isRightMouseButton(e.peer)) right_click()
-        else left_click()
-      }
-    }
-
-    def drag(info: (Point, List[Graph_Display.Node], List[Layout.Dummy]), to: Point)
-    {
-      val (from, p, d) = info
+      val (from, p, d) = draginfo
 
       val s = Transform.scale_discrete
-      val (dx, dy) = (to.x - from.x, to.y - from.y)
+      val dx = to.x - from.x
+      val dy = to.y - from.y
+
       (p, d) match {
         case (Nil, Nil) =>
           val r = panel.peer.getViewport.getViewRect
@@ -249,6 +227,35 @@
         case (ls, _) =>
           ls.foreach(l => visualizer.translate_vertex(Layout.Node(l), dx / s, dy / s))
       }
+
+      draginfo = (to, p, d)
+    }
+
+    def clicked(at: Point, m: Key.Modifiers, clicks: Int, right_click: Boolean)
+    {
+      val c = Transform.pane_to_graph_coordinates(at)
+
+      if (clicks < 2) {
+        if (right_click) {
+          val menu = Popups(panel, visualizer.find_node(c), visualizer.Selection.get())
+          menu.show(panel.peer, at.x, at.y)
+        }
+        else {
+          (visualizer.find_node(c), m) match {
+            case (Some(node), Key.Modifier.Control) => visualizer.Selection.add(node)
+            case (None, Key.Modifier.Control) =>
+
+            case (Some(node), Key.Modifier.Shift) => visualizer.Selection.add(node)
+            case (None, Key.Modifier.Shift) =>
+
+            case (Some(node), _) =>
+              visualizer.Selection.clear()
+              visualizer.Selection.add(node)
+            case (None, _) =>
+              visualizer.Selection.clear()
+          }
+        }
+      }
     }
   }
 }