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)))
+    }
+}
+