# HG changeset patch
# User wenzelm
# Date 1420401687 -3600
# Node ID 5cd92c743958b54daeed592320027bfb79161487
# Parent  5e72808149165a064e3e732040986399d873c637
explicit Layout.Point;
tuned signature;
tuned;

diff -r 5e7280814916 -r 5cd92c743958 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Sun Jan 04 16:45:41 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Sun Jan 04 21:01:27 2015 +0100
@@ -164,9 +164,7 @@
 
   object Mouse_Interaction
   {
-    type Dummy = (Graph_Display.Edge, Int)
-
-    private var draginfo: (Point, List[Graph_Display.Node], List[Dummy]) = null
+    private var draginfo: (Point, List[Graph_Display.Node], List[(Graph_Display.Edge, Int)]) = null
 
     val react: PartialFunction[Event, Unit] =
     {
@@ -178,19 +176,20 @@
       case e @ MouseClicked(_, p, m, n, _) => click(p, m, n, e)
     }
 
-    def dummy(at: Point2D): Option[Dummy] =
+    def dummy(at: Point2D): Option[(Graph_Display.Edge, Int)] =
     {
       val m = visualizer.metrics()
       visualizer.model.make_visible_graph().edges_iterator.map(
-        edge => visualizer.Coordinates(edge).zipWithIndex.map((edge, _))).flatten.find(
-          {
-            case (_, ((x, y), _)) =>
-              visualizer.Drawer.shape(m, Graph_Display.Node.dummy).
-                contains(at.getX() - x, at.getY() - y)
-          }) match {
-            case None => None
-            case Some((edge, (_, index))) => Some((edge, index))
-          }
+        edge =>
+          visualizer.Coordinates.get_dummies(edge).zipWithIndex.map((edge, _))).flatten.find(
+            {
+              case (_, (p, _)) =>
+                visualizer.Drawer.shape(m, Graph_Display.Node.dummy).
+                  contains(at.getX() - p.x, at.getY() - p.y)
+            }) match {
+              case None => None
+              case Some((edge, (_, index))) => Some((edge, index))
+            }
     }
 
     def pressed(at: Point)
@@ -248,9 +247,9 @@
       }
     }
 
-    def drag(draginfo: (Point, List[Graph_Display.Node], List[Dummy]), to: Point)
+    def drag(info: (Point, List[Graph_Display.Node], List[(Graph_Display.Edge, Int)]), to: Point)
     {
-      val (from, p, d) = draginfo
+      val (from, p, d) = info
 
       val s = Transform.scale_discrete
       val (dx, dy) = (to.x - from.x, to.y - from.y)
@@ -262,10 +261,10 @@
           paint_panel.peer.scrollRectToVisible(r)
 
         case (Nil, ds) =>
-          ds.foreach(d => visualizer.Coordinates.translate(d, (dx / s, dy / s)))
+          ds.foreach(d => visualizer.Coordinates.translate_dummy(d, dx / s, dy / s))
 
         case (ls, _) =>
-          ls.foreach(l => visualizer.Coordinates.translate(l, (dx / s, dy / s)))
+          ls.foreach(l => visualizer.Coordinates.translate_node(l, dx / s, dy / s))
       }
     }
   }
diff -r 5e7280814916 -r 5cd92c743958 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Sun Jan 04 16:45:41 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Sun Jan 04 21:01:27 2015 +0100
@@ -17,19 +17,17 @@
 import isabelle._
 
 
-final case class Layout(
-  nodes: Layout.Coordinates,
-  dummies: Map[Graph_Display.Edge, List[Layout.Point]])
-
 object Layout
 {
-  type Key = Graph_Display.Node
-  type Point = (Double, Double)
-  type Coordinates = Map[Key, Point]
-  type Level = List[Key]
-  type Levels = List[Level]
+  object Point { val zero: Point = Point(0.0, 0.0) }
+  case class Point(x: Double, y: Double)
 
-  val empty = Layout(Map.empty, Map.empty)
+  private type Key = Graph_Display.Node
+  private type Coordinates = Map[Key, Point]
+  private type Level = List[Key]
+  private type Levels = List[Level]
+
+  val empty = new Layout(Map.empty, Map.empty)
 
   val pendulum_iterations = 10
   val minimize_crossings_iterations = 40
@@ -68,7 +66,7 @@
         (((Map.empty[Key, Point], 0.0) /: levels) {
           case ((coords1, y), level) =>
             ((((coords1, 0.0) /: level) {
-              case ((coords2, x), key) => (coords2 + (key -> (x, y)), x + box_distance)
+              case ((coords2, x), key) => (coords2 + (key -> Point(x, y)), x + box_distance)
             })._1, y + box_height(level))
         })._1
 
@@ -79,7 +77,7 @@
           case (map, key) => map + (key -> dummies(key).map(coords(_)))
         }
 
-      Layout(coords, dummy_coords)
+      new Layout(coords, dummy_coords)
     }
   }
 
@@ -274,8 +272,8 @@
   {
     var nodes: List[Key] = List(node)
 
-    def left(coords: Coordinates): Double = nodes.iterator.map(coords(_)._1).min
-    def right(coords: Coordinates): Double = nodes.iterator.map(coords(_)._1).max
+    def left(coords: Coordinates): Double = nodes.iterator.map(coords(_).x).min
+    def right(coords: Coordinates): Double = nodes.iterator.map(coords(_).x).max
 
     def distance(coords: Coordinates, to: Region): Double =
       math.abs(left(coords) - to.left(coords)) min
@@ -284,15 +282,40 @@
     def deflection(coords: Coordinates, top_down: Boolean): Double =
       (for {
         k <- nodes.iterator
-        x = coords(k)._1
+        x = coords(k).x
         as = if (top_down) graph.imm_preds(k) else graph.imm_succs(k)
-      } yield as.iterator.map(coords(_)._1 - x).sum / (as.size max 1)).sum / nodes.length
+      } yield as.iterator.map(coords(_).x - x).sum / (as.size max 1)).sum / nodes.length
 
-    def move(coords: Coordinates, by: Double): Coordinates =
+    def move(coords: Coordinates, dx: Double): Coordinates =
       (coords /: nodes) {
         case (cs, node) =>
-          val (x, y) = cs(node)
-          cs + (node -> (x + by, y))
+          val p = cs(node)
+          cs + (node -> Point(p.x + dx, p.y))
       }
   }
 }
+
+final class Layout private(
+  nodes: Map[Graph_Display.Node, Layout.Point],
+  dummies: Map[Graph_Display.Edge, List[Layout.Point]])
+{
+  def get_node(node: Graph_Display.Node): Layout.Point =
+    nodes.getOrElse(node, Layout.Point.zero)
+
+  def map_node(node: Graph_Display.Node, f: Layout.Point => Layout.Point): Layout =
+    nodes.get(node) match {
+      case None => this
+      case Some(p) => new Layout(nodes + (node -> f(p)), dummies)
+    }
+
+
+  def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] =
+    dummies.getOrElse(edge, Nil)
+
+  def map_dummies(edge: Graph_Display.Edge, f: List[Layout.Point] => List[Layout.Point]): Layout =
+    dummies.get(edge) match {
+      case None => this
+      case Some(ds) => new Layout(nodes, dummies + (edge -> f(ds)))
+    }
+}
+
diff -r 5e7280814916 -r 5cd92c743958 src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Sun Jan 04 16:45:41 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Sun Jan 04 21:01:27 2015 +0100
@@ -24,11 +24,11 @@
     def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node)
       : Rectangle2D.Double =
     {
-      val (x, y) = visualizer.Coordinates(node)
+      val p = visualizer.Coordinates.get_node(node)
       val bounds = m.string_bounds(node.toString)
       val w = bounds.getWidth + m.pad
       val h = bounds.getHeight + m.pad
-      new Rectangle2D.Double((x - (w / 2)).floor, (y - (h / 2)).floor, w.ceil, h.ceil)
+      new Rectangle2D.Double((p.x - (w / 2)).floor, (p.y - (h / 2)).floor, w.ceil, h.ceil)
     }
 
     def paint(gfx: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node)
@@ -81,28 +81,23 @@
     def paint(gfx: Graphics2D, visualizer: Visualizer,
       edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
     {
-      val (fx, fy) = visualizer.Coordinates(edge._1)
-      val (tx, ty) = visualizer.Coordinates(edge._2)
+      val p = visualizer.Coordinates.get_node(edge._1)
+      val q = visualizer.Coordinates.get_node(edge._2)
       val ds =
       {
-        val min = fy min ty
-        val max = fy max ty
-        visualizer.Coordinates(edge).filter({ case (_, y) => min < y && y < max })
+        val a = p.y min q.y
+        val b = p.y max q.y
+        visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b)
       }
       val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
 
-      path.moveTo(fx, fy)
-      ds.foreach({ case (x, y) => path.lineTo(x, y) })
-      path.lineTo(tx, ty)
+      path.moveTo(p.x, p.y)
+      ds.foreach(d => path.lineTo(d.x, d.y))
+      path.lineTo(q.x, q.y)
 
-      if (dummies) {
-        ds.foreach({
-            case (x, y) => {
-              val at = AffineTransform.getTranslateInstance(x, y)
-              Dummy.paint_transformed(gfx, visualizer, at)
-            }
-          })
-      }
+      if (dummies)
+        ds.foreach(d =>
+          Dummy.paint_transformed(gfx, visualizer, AffineTransform.getTranslateInstance(d.x, d.y)))
 
       gfx.setStroke(default_stroke)
       gfx.setColor(visualizer.edge_color(edge))
@@ -121,48 +116,45 @@
     def paint(gfx: Graphics2D, visualizer: Visualizer,
       edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
     {
-      val (fx, fy) = visualizer.Coordinates(edge._1)
-      val (tx, ty) = visualizer.Coordinates(edge._2)
+      val p = visualizer.Coordinates.get_node(edge._1)
+      val q = visualizer.Coordinates.get_node(edge._2)
       val ds =
       {
-        val min = fy min ty
-        val max = fy max ty
-        visualizer.Coordinates(edge).filter({ case (_, y) => min < y && y < max })
+        val a = p.y min q.y
+        val b = p.y max q.y
+        visualizer.Coordinates.get_dummies(edge).filter(d => a < d.y && d.y < b)
       }
 
       if (ds.isEmpty) Straight_Edge.paint(gfx, visualizer, edge, head, dummies)
       else {
         val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
-        path.moveTo(fx, fy)
+        path.moveTo(p.x, p.y)
 
-        val coords = ((fx, fy) :: ds ::: List((tx, ty)))
-        val (dx, dy) = (coords(2)._1 - coords(0)._1, coords(2)._2 - coords(0)._2)
+        val coords = p :: ds ::: List(q)
+        val dx = coords(2).x - coords(0).x
+        val dy = coords(2).y - coords(0).y
 
         val (dx2, dy2) =
-          ((dx, dy) /: coords.sliding(3))({
-            case ((dx, dy), List((lx, ly), (mx, my), (rx, ry))) => {
-              val (dx2, dy2) = (rx - lx, ry - ly)
-
-              path.curveTo(lx + slack * dx , ly + slack * dy,
-                           mx - slack * dx2, my - slack * dy2,
-                           mx              , my)
+          ((dx, dy) /: coords.sliding(3)) {
+            case ((dx, dy), List(l, m, r)) =>
+              val dx2 = r.x - l.x
+              val dy2 = r.y - l.y
+              path.curveTo(
+                l.x + slack * dx, l.y + slack * dy,
+                m.x - slack * dx2, m.y - slack * dy2,
+                m.x, m.y)
               (dx2, dy2)
-            }
-          })
+          }
 
-        val (lx, ly) = ds.last
-        path.curveTo(lx + slack * dx2, ly + slack * dy2,
-                     tx - slack * dx2, ty - slack * dy2,
-                     tx              , ty)
+        val l = ds.last
+        path.curveTo(
+          l.x + slack * dx2, l.y + slack * dy2,
+          q.x - slack * dx2, q.y - slack * dy2,
+          q.x, q.y)
 
-        if (dummies) {
-          ds.foreach({
-              case (x, y) => {
-                val at = AffineTransform.getTranslateInstance(x, y)
-                Dummy.paint_transformed(gfx, visualizer, at)
-              }
-            })
-        }
+        if (dummies)
+          ds.foreach(d =>
+            Dummy.paint_transformed(gfx, visualizer, AffineTransform.getTranslateInstance(d.x, d.y)))
 
         gfx.setStroke(default_stroke)
         gfx.setColor(visualizer.edge_color(edge))
diff -r 5e7280814916 -r 5cd92c743958 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Sun Jan 04 16:45:41 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sun Jan 04 21:01:27 2015 +0100
@@ -103,44 +103,27 @@
 
   object Coordinates
   {
+    // owned by GUI thread
     private var layout = Layout.empty
 
-    def apply(node: Graph_Display.Node): (Double, Double) =
-      layout.nodes.getOrElse(node, (0.0, 0.0))
+    def get_node(node: Graph_Display.Node): Layout.Point = layout.get_node(node)
+    def get_dummies(edge: Graph_Display.Edge): List[Layout.Point] = layout.get_dummies(edge)
 
-    def apply(edge: Graph_Display.Edge): List[(Double, Double)] =
-      layout.dummies.getOrElse(edge, Nil)
-
-    def reposition(node: Graph_Display.Node, to: (Double, Double))
+    def translate_node(node: Graph_Display.Node, dx: Double, dy: Double)
     {
-      layout = layout.copy(nodes = layout.nodes + (node -> to))
+      layout = layout.map_node(node, p => Layout.Point(p.x + dx, p.y + dy))
     }
 
-    def reposition(d: (Graph_Display.Edge, Int), to: (Double, Double))
+    def translate_dummy(d: (Graph_Display.Edge, Int), dx: Double, dy: Double)
     {
-      val (e, index) = d
-      layout.dummies.get(e) match {
-        case None =>
-        case Some(ds) =>
-          layout = layout.copy(dummies =
-            layout.dummies + (e ->
-              (ds.zipWithIndex :\ List.empty[(Double, Double)]) {
-                case ((t, i), n) => if (index == i) to :: n else t :: n
-              }))
-      }
-    }
-
-    def translate(node: Graph_Display.Node, by: (Double, Double))
-    {
-      val ((x, y), (dx, dy)) = (Coordinates(node), by)
-      reposition(node, (x + dx, y + dy))
-    }
-
-    def translate(d: (Graph_Display.Edge, Int), by: (Double, Double))
-    {
-      val ((e, i), (dx, dy)) = (d, by)
-      val (x, y) = apply(e)(i)
-      reposition(d, (x + dx, y + dy))
+      val (edge, index) = d
+      layout = layout.map_dummies(edge,
+        ds => {
+          val p = ds(index)
+          (ds.zipWithIndex :\ List.empty[Layout.Point]) {
+            case ((t, i), n) => if (index == i) Layout.Point(p.x + dx, p.y + dy) :: n else t :: n
+          }
+        })
     }
 
     def update_layout()