# HG changeset patch
# User wenzelm
# Date 1420312947 -3600
# Node ID be4180f3c236d076486491fb4cd3ae2be4f39c6f
# Parent  19b5fc4b2b3887ec62fde6ee21a087e1fe980f04
more formal Graph_Display.Node (with ordering) and Graph_Display.Edge;
misc tuning;
tuned signature;

diff -r 19b5fc4b2b38 -r be4180f3c236 src/Pure/General/graph.scala
--- a/src/Pure/General/graph.scala	Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Pure/General/graph.scala	Sat Jan 03 20:22:27 2015 +0100
@@ -21,15 +21,13 @@
   def empty[Key, A](implicit ord: Ordering[Key]): Graph[Key, A] =
     new Graph[Key, A](SortedMap.empty(ord))
 
-  def make[Key, A](entries: List[((Key, A), List[Key])], converse: Boolean = false)(
+  def make[Key, A](entries: List[((Key, A), List[Key])])(
     implicit ord: Ordering[Key]): Graph[Key, A] =
   {
     val graph1 =
       (empty[Key, A](ord) /: entries) { case (graph, ((x, info), _)) => graph.new_node(x, info) }
     val graph2 =
-      (graph1 /: entries) { case (graph, ((x, _), ys)) =>
-        if (converse) (graph /: ys)(_.add_edge(_, x)) else (graph /: ys)(_.add_edge(x, _))
-      }
+      (graph1 /: entries) { case (graph, ((x, _), ys)) => (graph /: ys)(_.add_edge(x, _)) }
     graph2
   }
 
@@ -46,11 +44,11 @@
       list(pair(pair(key, info), list(key)))(graph.dest)
     })
 
-  def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A], converse: Boolean = false)(
+  def decode[Key, A](key: XML.Decode.T[Key], info: XML.Decode.T[A])(
     implicit ord: Ordering[Key]): XML.Decode.T[Graph[Key, A]] =
     ((body: XML.Body) => {
       import XML.Decode._
-      make(list(pair(pair(key, info), list(key)))(body), converse)(ord)
+      make(list(pair(pair(key, info), list(key)))(body))(ord)
     })
 }
 
diff -r 19b5fc4b2b38 -r be4180f3c236 src/Pure/General/graph_display.scala
--- a/src/Pure/General/graph_display.scala	Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Pure/General/graph_display.scala	Sat Jan 03 20:22:27 2015 +0100
@@ -13,56 +13,52 @@
   type Entry = ((String, (String, XML.Body)), List[String])
 
 
-  /* node names */
+  /* graph structure */
 
-  object Name
+  object Node
   {
-    val dummy: Name = Name("", "")
+    val dummy: Node = Node("", "")
 
-    object Ordering extends scala.math.Ordering[Name]
+    object Ordering extends scala.math.Ordering[Node]
     {
-      def compare(name1: Name, name2: Name): Int =
-        name1.name compare name2.name match {
-          case 0 => name1.ident compare name2.ident
+      def compare(node1: Node, node2: Node): Int =
+        node1.name compare node2.name match {
+          case 0 => node1.ident compare node2.ident
           case ord => ord
         }
     }
   }
-
-  sealed case class Name(name: String, ident: String)
+  sealed case class Node(name: String, ident: String)
   {
+    def is_dummy: Boolean = this == Node.dummy
     override def toString: String = name
   }
 
-
-  /* graph structure */
+  type Edge = (Node, Node)
 
-  type Graph = isabelle.Graph[Name, XML.Body]
+  type Graph = isabelle.Graph[Node, XML.Body]
 
-  val empty_graph: Graph = isabelle.Graph.empty(Name.Ordering)
+  val empty_graph: Graph = isabelle.Graph.empty(Node.Ordering)
 
   def build_graph(entries: List[Entry]): Graph =
   {
-    val the_key =
-      (Map.empty[String, Name] /: entries) {
-        case (m, ((ident, (name, _)), _)) => m + (ident -> Name(name, ident))
+    val node =
+      (Map.empty[String, Node] /: entries) {
+        case (m, ((ident, (name, _)), _)) => m + (ident -> Node(name, ident))
       }
     (((empty_graph /: entries) {
-        case (g, ((ident, (_, content)), _)) => g.new_node(the_key(ident), content)
+        case (g, ((ident, (_, content)), _)) => g.new_node(node(ident), content)
       }) /: entries) {
         case (g1, ((ident, _), parents)) =>
-          (g1 /: parents) { case (g2, parent) => g2.add_edge(the_key(parent), the_key(ident)) }
+          (g1 /: parents) { case (g2, parent) => g2.add_edge(node(parent), node(ident)) }
       }
   }
 
   def decode_graph(body: XML.Body): Graph =
-  {
-    val entries =
-    {
-      import XML.Decode._
-      list(pair(pair(string, pair(string, x => x)), list(string)))(body)
-    }
-    build_graph(entries)
-  }
+    build_graph(
+      {
+        import XML.Decode._
+        list(pair(pair(string, pair(string, x => x)), list(string)))(body)
+      })
 }
 
diff -r 19b5fc4b2b38 -r be4180f3c236 src/Tools/Graphview/graph_panel.scala
--- a/src/Tools/Graphview/graph_panel.scala	Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/graph_panel.scala	Sat Jan 03 20:22:27 2015 +0100
@@ -27,9 +27,9 @@
 
   override lazy val peer: JScrollPane = new JScrollPane with SuperMixin {
     override def getToolTipText(event: java.awt.event.MouseEvent): String =
-      node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
-        case Some(name) =>
-          visualizer.model.complete_graph.get_node(name).content match {
+      find_node(Transform.pane_to_graph_coordinates(event.getPoint)) match {
+        case Some(node) =>
+          visualizer.model.complete_graph.get_node(node) match {
             case Nil => null
             case content => visualizer.make_tooltip(panel.peer, event.getX, event.getY, content)
           }
@@ -45,11 +45,11 @@
 
   peer.getVerticalScrollBar.setUnitIncrement(10)
 
-  def node(at: Point2D): Option[String] =
+  def find_node(at: Point2D): Option[Graph_Display.Node] =
   {
     val m = visualizer.metrics()
     visualizer.model.visible_nodes_iterator
-      .find(name => visualizer.Drawer.shape(m, Some(name)).contains(at))
+      .find(node => visualizer.Drawer.shape(m, node).contains(at))
   }
 
   def refresh()
@@ -181,9 +181,9 @@
 
     object Mouse
     {
-      type Dummy = ((String, String), Int)
+      type Dummy = (Graph_Display.Edge, Int)
 
-      private var draginfo: (Point, Iterable[String], Iterable[Dummy]) = null
+      private var draginfo: (Point, List[Graph_Display.Node], List[Dummy]) = null
 
       val react: PartialFunction[Event, Unit] =
       {
@@ -199,23 +199,27 @@
       {
         val m = visualizer.metrics()
         visualizer.model.visible_edges_iterator.map(
-          i => visualizer.Coordinates(i).zipWithIndex.map((i, _))).flatten.find({
-            case (_, ((x, y), _)) =>
-              visualizer.Drawer.shape(m, None).contains(at.getX() - x, at.getY() - y)
-          }) match {
-            case None => None
-            case Some((name, (_, index))) => Some((name, index))
-          }
+          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))
+            }
       }
 
       def pressed(at: Point)
       {
         val c = Transform.pane_to_graph_coordinates(at)
-        val l = node(c) match {
-          case Some(l) =>
-            if (visualizer.Selection(l)) visualizer.Selection() else List(l)
-          case None => Nil
-        }
+        val l =
+          find_node(c) match {
+            case Some(node) =>
+              if (visualizer.Selection.contains(node)) visualizer.Selection.get()
+              else List(node)
+            case None => Nil
+          }
         val d =
           l match {
             case Nil =>
@@ -231,25 +235,27 @@
       def click(at: Point, m: Key.Modifiers, clicks: Int, e: MouseEvent)
       {
         val c = Transform.pane_to_graph_coordinates(at)
-        val p = node(c)
 
         def left_click()
         {
-          (p, m) match {
-            case (Some(l), Key.Modifier.Control) => visualizer.Selection.add(l)
+          (find_node(c), m) match {
+            case (Some(node), Key.Modifier.Control) => visualizer.Selection.add(node)
             case (None, Key.Modifier.Control) =>
 
-            case (Some(l), Key.Modifier.Shift) => visualizer.Selection.add(l)
+            case (Some(node), Key.Modifier.Shift) => visualizer.Selection.add(node)
             case (None, Key.Modifier.Shift) =>
 
-            case (Some(l), _) => visualizer.Selection.set(List(l))
-            case (None, _) => visualizer.Selection.clear
+            case (Some(node), _) =>
+              visualizer.Selection.clear()
+              visualizer.Selection.add(node)
+            case (None, _) =>
+              visualizer.Selection.clear()
           }
         }
 
         def right_click()
         {
-          val menu = Popups(panel, p, visualizer.Selection())
+          val menu = Popups(panel, find_node(c), visualizer.Selection.get())
           menu.show(panel.peer, at.x, at.y)
         }
 
@@ -259,7 +265,7 @@
         }
       }
 
-      def drag(draginfo: (Point, Iterable[String], Iterable[Dummy]), to: Point)
+      def drag(draginfo: (Point, List[Graph_Display.Node], List[Dummy]), to: Point)
       {
         val (from, p, d) = draginfo
 
diff -r 19b5fc4b2b38 -r be4180f3c236 src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/layout.scala	Sat Jan 03 20:22:27 2015 +0100
@@ -13,23 +13,22 @@
 
 final case class Layout(
   nodes: Layout.Coordinates,
-  dummies: Map[(Layout.Key, Layout.Key), List[Layout.Point]])
+  dummies: Map[Graph_Display.Edge, List[Layout.Point]])
 
 object Layout
 {
-  type Key = String
+  type Key = Graph_Display.Node
   type Point = (Double, Double)
   type Coordinates = Map[Key, Point]
   type Level = List[Key]
   type Levels = List[Level]
-  type Dummies = (Model.Graph, List[Key], Map[Key, Int])
 
   val empty = Layout(Map.empty, Map.empty)
 
   val pendulum_iterations = 10
   val minimize_crossings_iterations = 40
 
-  def make(graph: Model.Graph, box_distance: Double, box_height: Int => Double): Layout =
+  def make(graph: Graph_Display.Graph, box_distance: Double, box_height: Int => Double): Layout =
   {
     if (graph.is_empty) empty
     else {
@@ -54,9 +53,7 @@
         (((Map.empty[Key, Point], 0.0) /: levels) {
           case ((coords1, y), level) =>
             ((((coords1, 0.0) /: level) {
-              case ((coords2, x), key) =>
-                val s = if (graph.defined(key)) graph.get_node(key).name else "X"
-                (coords2 + (key -> (x, y)), x + box_distance)
+              case ((coords2, x), key) => (coords2 + (key -> (x, y)), x + box_distance)
             })._1, y + box_height(level.length))
         })._1
 
@@ -72,18 +69,22 @@
   }
 
 
-  def add_dummies(graph: Model.Graph, from: Key, to: Key, levels: Map[Key, Int]): Dummies =
+  def add_dummies(graph: Graph_Display.Graph, from: Key, to: Key, levels: Map[Key, Int])
+    : (Graph_Display.Graph, List[Key], Map[Key, Int]) =
   {
     val ds =
-      ((levels(from) + 1) until levels(to))
-      .map("%s$%s$%d" format (from, to, _)).toList
+      ((levels(from) + 1) until levels(to)).map(l => {
+          // FIXME !?
+          val ident = "%s$%s$%d".format(from.ident, to.ident, l)
+          Graph_Display.Node(ident, ident)
+        }).toList
 
     val ls =
       (levels /: ((levels(from) + 1) until levels(to)).zip(ds)) {
         case (ls, (l, d)) => ls + (d -> l)
       }
 
-    val graph1 = (graph /: ds)(_.new_node(_, Model.empty_info))
+    val graph1 = (graph /: ds)(_.new_node(_, Nil))
     val graph2 =
       (graph1.del_edge(from, to) /: (from :: ds ::: List(to)).sliding(2)) {
         case (g, List(x, y)) => g.add_edge(x, y)
@@ -91,7 +92,7 @@
     (graph2, ds, ls)
   }
 
-  def level_map(graph: Model.Graph): Map[Key, Int] =
+  def level_map(graph: Graph_Display.Graph): Map[Key, Int] =
     (Map.empty[Key, Int] /: graph.topological_order) {
       (levels, key) => {
         val lev = 1 + (-1 /: graph.imm_preds(key)) { case (m, key) => m max levels(key) }
@@ -105,10 +106,10 @@
     val buckets = new Array[Level](max_lev + 1)
     for (l <- 0 to max_lev) { buckets(l) = Nil }
     for ((key, l) <- map) { buckets(l) = key :: buckets(l) }
-    buckets.iterator.map(_.sorted).toList
+    buckets.iterator.map(_.sorted(Graph_Display.Node.Ordering)).toList
   }
 
-  def count_crossings(graph: Model.Graph, levels: Levels): Int =
+  def count_crossings(graph: Graph_Display.Graph, levels: Levels): Int =
   {
     def in_level(ls: Levels): Int = ls match {
       case List(top, bot) =>
@@ -131,7 +132,7 @@
     levels.iterator.sliding(2).map(ls => in_level(ls.toList)).sum
   }
 
-  def minimize_crossings(graph: Model.Graph, levels: Levels): Levels =
+  def minimize_crossings(graph: Graph_Display.Graph, levels: Levels): Levels =
   {
     def resort_level(parent: Level, child: Level, top_down: Boolean): Level =
       child.map(k => {
@@ -165,7 +166,7 @@
     }._1
   }
 
-  def pendulum(graph: Model.Graph, box_distance: Double,
+  def pendulum(graph: Graph_Display.Graph, box_distance: Double,
     levels: Levels, coords: Map[Key, Point]): Coordinates =
   {
     type Regions = List[List[Region]]
@@ -251,7 +252,7 @@
     }._2
   }
 
-  private class Region(val graph: Model.Graph, node: Key)
+  private class Region(val graph: Graph_Display.Graph, node: Key)
   {
     var nodes: List[Key] = List(node)
 
diff -r 19b5fc4b2b38 -r be4180f3c236 src/Tools/Graphview/model.scala
--- a/src/Tools/Graphview/model.scala	Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/model.scala	Sat Jan 03 20:22:27 2015 +0100
@@ -33,39 +33,14 @@
 }
 
 
-object Model
-{
-  /* node info */
-
-  sealed case class Info(name: String, content: XML.Body)
-
-  val empty_info: Info = Info("", Nil)
-
-  val decode_info: XML.Decode.T[Info] = (body: XML.Body) =>
-  {
-    import XML.Decode._
-
-    val (name, content) = pair(string, x => x)(body)
-    Info(name, content)
-  }
-
-
-  /* graph */
-
-  type Graph = isabelle.Graph[String, Info]
-
-  val decode_graph: XML.Decode.T[Graph] =
-    isabelle.Graph.decode(XML.Decode.string, decode_info, converse = true)
-}
-
-class Model(val complete_graph: Model.Graph)
+class Model(val complete_graph: Graph_Display.Graph)
 {
   val Mutators =
     new Mutator_Container(
       List(
         Mutator.Node_Expression(".*", false, false, false),
         Mutator.Node_List(Nil, false, false, false),
-        Mutator.Edge_Endpoints("", ""),
+        Mutator.Edge_Endpoints(Graph_Display.Node.dummy, Graph_Display.Node.dummy),
         Mutator.Add_Node_Expression(""),
         Mutator.Add_Transitive_Closure(true, true)))
 
@@ -75,26 +50,29 @@
         Mutator.Node_Expression(".*", false, false, false),
         Mutator.Node_List(Nil, false, false, false)))
 
-  def visible_nodes_iterator: Iterator[String] = current_graph.keys_iterator
+  def find_node(ident: String): Option[Graph_Display.Node] =
+    complete_graph.keys_iterator.find(node => node.ident == ident)
 
-  def visible_edges_iterator: Iterator[(String, String)] =
+  def visible_nodes_iterator: Iterator[Graph_Display.Node] = current_graph.keys_iterator
+
+  def visible_edges_iterator: Iterator[Graph_Display.Edge] =
     current_graph.keys_iterator.flatMap(k => current_graph.imm_succs(k).iterator.map((k, _)))
 
-  def current_graph: Model.Graph =
+  def current_graph: Graph_Display.Graph =
     (complete_graph /: Mutators()) {
       case (g, m) => if (!m.enabled) g else m.mutator.mutate(complete_graph, g)
     }
 
-  private var _colors = Map.empty[String, Color]
+  private var _colors = Map.empty[Graph_Display.Node, Color]
   def colors = _colors
 
   private def build_colors()
   {
     _colors =
-      (Map.empty[String, Color] /: Colors()) {
+      (Map.empty[Graph_Display.Node, Color] /: Colors()) {
         case (colors, m) =>
           (colors /: m.mutator.mutate(complete_graph, complete_graph).keys_iterator) {
-            case (colors, k) => colors + (k -> m.color)
+            case (colors, node) => colors + (node -> m.color)
           }
       }
   }
diff -r 19b5fc4b2b38 -r be4180f3c236 src/Tools/Graphview/mutator.scala
--- a/src/Tools/Graphview/mutator.scala	Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/mutator.scala	Sat Jan 03 20:22:27 2015 +0100
@@ -24,30 +24,30 @@
   class Graph_Filter(
     val name: String,
     val description: String,
-    pred: Model.Graph => Model.Graph) extends Filter
+    pred: Graph_Display.Graph => Graph_Display.Graph) extends Filter
   {
-    def filter(graph: Model.Graph) : Model.Graph = pred(graph)
+    def filter(graph: Graph_Display.Graph): Graph_Display.Graph = pred(graph)
   }
 
   class Graph_Mutator(
     val name: String,
     val description: String,
-    pred: (Model.Graph, Model.Graph) => Model.Graph) extends Mutator
+    pred: (Graph_Display.Graph, Graph_Display.Graph) => Graph_Display.Graph) extends Mutator
   {
-    def mutate(complete_graph: Model.Graph, graph: Model.Graph): Model.Graph =
+    def mutate(complete_graph: Graph_Display.Graph, graph: Graph_Display.Graph): Graph_Display.Graph =
       pred(complete_graph, graph)
   }
 
   class Node_Filter(
     name: String,
     description: String,
-    pred: (Model.Graph, String) => Boolean)
+    pred: (Graph_Display.Graph, Graph_Display.Node) => Boolean)
     extends Graph_Filter(name, description, g => g.restrict(pred(g, _)))
 
   class Edge_Filter(
     name: String,
     description: String,
-    pred: (Model.Graph, String, String) => Boolean)
+    pred: (Graph_Display.Graph, Graph_Display.Node, Graph_Display.Node) => Boolean)
     extends Graph_Filter(
       name,
       description,
@@ -63,7 +63,7 @@
     reverse: Boolean,
     parents: Boolean,
     children: Boolean,
-    pred: (Model.Graph, String) => Boolean)
+    pred: (Graph_Display.Graph, Graph_Display.Node) => Boolean)
     extends Node_Filter(
       name,
       description,
@@ -90,10 +90,10 @@
       reverse,
       parents,
       children,
-      (g, k) => (regex.r findFirstIn k).isDefined)
+      (g, node) => (regex.r findFirstIn node.toString).isDefined)
 
   case class Node_List(
-    list: List[String],
+    list: List[Graph_Display.Node],
     reverse: Boolean,
     parents: Boolean,
     children: Boolean)
@@ -103,15 +103,16 @@
       reverse,
       parents,
       children,
-      (g, k) => list.exists(_ == k))
+      (g, node) => list.contains(node))
 
-  case class Edge_Endpoints(source: String, dest: String)
+  case class Edge_Endpoints(source: Graph_Display.Node, dest: Graph_Display.Node)
     extends Edge_Filter(
       "Hide edge",
       "Hides the edge whose endpoints match strings.",
       (g, s, d) => !(s == source && d == dest))
 
-  private def add_node_group(from: Model.Graph, to: Model.Graph, keys: List[String]) =
+  private def add_node_group(from: Graph_Display.Graph, to: Graph_Display.Graph,
+    keys: List[Graph_Display.Node]) =
   {
     // Add Nodes
     val with_nodes =
@@ -120,7 +121,7 @@
     // Add Edges
     (with_nodes /: keys) {
       (gv, key) => {
-        def add_edges(g: Model.Graph, keys: SortedSet[String], succs: Boolean) =
+        def add_edges(g: Graph_Display.Graph, keys: from.Keys, succs: Boolean) =
           (g /: keys) {
             (graph, end) => {
               if (!graph.keys_iterator.contains(end)) graph
@@ -145,7 +146,7 @@
       "Adds all relevant edges.",
       (complete_graph, graph) =>
         add_node_group(complete_graph, graph,
-          complete_graph.keys.filter(k => (regex.r findFirstIn k).isDefined).toList))
+          complete_graph.keys.filter(node => (regex.r findFirstIn node.toString).isDefined).toList))
 
   case class Add_Transitive_Closure(parents: Boolean, children: Boolean)
     extends Graph_Mutator(
@@ -165,13 +166,13 @@
 {
   val name: String
   val description: String
-  def mutate(complete_graph: Model.Graph, graph: Model.Graph): Model.Graph
+  def mutate(complete_graph: Graph_Display.Graph, graph: Graph_Display.Graph): Graph_Display.Graph
 
   override def toString: String = name
 }
 
 trait Filter extends Mutator
 {
-  def mutate(complete_graph: Model.Graph, graph: Model.Graph) = filter(graph)
-  def filter(graph: Model.Graph) : Model.Graph
+  def mutate(complete_graph: Graph_Display.Graph, graph: Graph_Display.Graph) = filter(graph)
+  def filter(graph: Graph_Display.Graph): Graph_Display.Graph
 }
diff -r 19b5fc4b2b38 -r be4180f3c236 src/Tools/Graphview/mutator_dialog.scala
--- a/src/Tools/Graphview/mutator_dialog.scala	Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/mutator_dialog.scala	Sat Jan 03 20:22:27 2015 +0100
@@ -246,6 +246,7 @@
 
     def get_mutator: Mutator.Info =
     {
+      val model = visualizer.model
       val m =
         initials.mutator match {
           case Mutator.Identity() =>
@@ -260,15 +261,21 @@
               inputs(0)._2.bool)
           case Mutator.Node_List(_, _, _, _) =>
             Mutator.Node_List(
-              inputs(2)._2.string.split(',').filter(_ != "").toList,
+              for {
+                ident <- space_explode(',', inputs(2)._2.string)
+                node <- model.find_node(ident)
+              } yield node,
               inputs(3)._2.bool,
               // "Parents" means "Show parents" or "Matching Children"
               inputs(1)._2.bool,
               inputs(0)._2.bool)
           case Mutator.Edge_Endpoints(_, _) =>
-            Mutator.Edge_Endpoints(
-              inputs(0)._2.string,
-              inputs(1)._2.string)
+            (model.find_node(inputs(0)._2.string), model.find_node(inputs(1)._2.string)) match {
+              case (Some(node1), Some(node2)) =>
+                Mutator.Edge_Endpoints(node1, node2)
+              case _ =>
+                Mutator.Identity()
+            }
           case Mutator.Add_Node_Expression(r) =>
             val r1 = inputs(0)._2.string
             Mutator.Add_Node_Expression(if (Library.make_regex(r1).isDefined) r1 else r)
@@ -295,12 +302,12 @@
           List(
             ("", new Check_Box_Input("Parents", check_children)),
             ("", new Check_Box_Input("Children", check_parents)),
-            ("Names", new Text_Field_Input(list.mkString(","))),
+            ("Names", new Text_Field_Input(list.map(_.ident).mkString(","))),
             ("", new Check_Box_Input(reverse_caption, reverse)))
         case Mutator.Edge_Endpoints(source, dest) =>
           List(
-            ("Source", new Text_Field_Input(source)),
-            ("Destination", new Text_Field_Input(dest)))
+            ("Source", new Text_Field_Input(source.ident)),
+            ("Destination", new Text_Field_Input(dest.ident)))
         case Mutator.Add_Node_Expression(regex) =>
           List(("Regex", new Text_Field_Input(regex, x => Library.make_regex(x).isDefined)))
         case Mutator.Add_Transitive_Closure(parents, children) =>
diff -r 19b5fc4b2b38 -r be4180f3c236 src/Tools/Graphview/popups.scala
--- a/src/Tools/Graphview/popups.scala	Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/popups.scala	Sat Jan 03 20:22:27 2015 +0100
@@ -16,46 +16,50 @@
 
 object Popups
 {
-  def apply(panel: Graph_Panel, under_mouse: Option[String], selected: List[String]): JPopupMenu =
+  def apply(
+    panel: Graph_Panel,
+    mouse_node: Option[Graph_Display.Node],
+    selected_nodes: List[Graph_Display.Node]): JPopupMenu =
   {
     val visualizer = panel.visualizer
 
     val add_mutator = visualizer.model.Mutators.add _
     val curr = visualizer.model.current_graph
 
-    def filter_context(ls: List[String], reverse: Boolean, caption: String, edges: Boolean) =
+    def filter_context(
+        nodes: List[Graph_Display.Node], reverse: Boolean, caption: String, edges: Boolean) =
       new Menu(caption) {
         contents +=
           new MenuItem(new Action("This") {
             def apply =
-              add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, false, false)))
+              add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, false, false)))
           })
 
         contents +=
           new MenuItem(new Action("Family") {
             def apply =
-              add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, true, true)))
+              add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, true, true)))
           })
 
         contents +=
           new MenuItem(new Action("Parents") {
             def apply =
-              add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, false, true)))
+              add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, false, true)))
           })
 
         contents +=
           new MenuItem(new Action("Children") {
             def apply =
-              add_mutator(Mutator.make(visualizer, Mutator.Node_List(ls, reverse, true, false)))
+              add_mutator(Mutator.make(visualizer, Mutator.Node_List(nodes, reverse, true, false)))
           })
 
         if (edges) {
           val outs =
-            ls.map(l => (l, curr.imm_succs(l)))  // FIXME iterator
-              .filter(_._2.size > 0).sortBy(_._1)
+            nodes.map(l => (l, curr.imm_succs(l)))  // FIXME iterator
+              .filter(_._2.size > 0).sortBy(_._1)(Graph_Display.Node.Ordering)
           val ins =
-            ls.map(l => (l, curr.imm_preds(l)))  // FIXME iterator
-              .filter(_._2.size > 0).sortBy(_._1)
+            nodes.map(l => (l, curr.imm_preds(l)))  // FIXME iterator
+              .filter(_._2.size > 0).sortBy(_._1)(Graph_Display.Node.Ordering)
 
           if (outs.nonEmpty || ins.nonEmpty) {
             contents += new Separator()
@@ -68,13 +72,13 @@
                   outs.map(e => {
                     val (from, tos) = e
                     contents +=
-                      new Menu(from) {
+                      new Menu(from.toString) {
                         contents += new MenuItem("To...") { enabled = false }
 
-                        tos.toList.sorted.distinct.map(to => {
+                        tos.toList.sorted(Graph_Display.Node.Ordering).distinct.map(to => {
                           contents +=
                             new MenuItem(
-                              new Action(to) {
+                              new Action(to.toString) {
                                 def apply =
                                   add_mutator(
                                     Mutator.make(visualizer, Mutator.Edge_Endpoints(from, to)))
@@ -90,13 +94,13 @@
                   ins.map(e => {
                     val (to, froms) = e
                     contents +=
-                      new Menu(to) {
+                      new Menu(to.toString) {
                         contents += new MenuItem("From...") { enabled = false }
 
-                        froms.toList.sorted.distinct.map(from => {
+                        froms.toList.sorted(Graph_Display.Node.Ordering).distinct.map(from => {
                           contents +=
                             new MenuItem(
-                              new Action(from) {
+                              new Action(from.toString) {
                                 def apply =
                                   add_mutator(
                                     Mutator.make(visualizer, Mutator.Edge_Endpoints(from, to)))
@@ -114,30 +118,27 @@
 
     popup.add(
       new MenuItem(
-        new Action("Remove all filters") {
-          def apply = visualizer.model.Mutators(Nil)
-        }).peer)
+        new Action("Remove all filters") { def apply = visualizer.model.Mutators(Nil) }).peer)
     popup.add(new JPopupMenu.Separator)
 
-    if (under_mouse.isDefined) {
-      val v = under_mouse.get
-      popup.add(
-        new MenuItem("Mouseover: %s".format(visualizer.Caption(v))) { enabled = false }.peer)
+    if (mouse_node.isDefined) {
+      val node = mouse_node.get
+      popup.add(new MenuItem("Mouseover: " + node) { enabled = false }.peer)
 
-      popup.add(filter_context(List(v), true, "Hide", true).peer)
-      popup.add(filter_context(List(v), false, "Show only", false).peer)
+      popup.add(filter_context(List(node), true, "Hide", true).peer)
+      popup.add(filter_context(List(node), false, "Show only", false).peer)
 
       popup.add(new JPopupMenu.Separator)
     }
-    if (!selected.isEmpty) {
+    if (!selected_nodes.isEmpty) {
       val text =
-        if (selected.length > 1) "Multiple"
-        else visualizer.Caption(selected.head)
+        if (selected_nodes.length > 1) "Multiple"
+        else selected_nodes.head.toString
 
-      popup.add(new MenuItem("Selected: %s".format(text)) { enabled = false }.peer)
+      popup.add(new MenuItem("Selected: " + text) { enabled = false }.peer)
 
-      popup.add(filter_context(selected, true, "Hide", true).peer)
-      popup.add(filter_context(selected, false, "Show only", false).peer)
+      popup.add(filter_context(selected_nodes, true, "Hide", true).peer)
+      popup.add(filter_context(selected_nodes, false, "Show only", false).peer)
       popup.add(new JPopupMenu.Separator)
     }
 
diff -r 19b5fc4b2b38 -r be4180f3c236 src/Tools/Graphview/shapes.scala
--- a/src/Tools/Graphview/shapes.scala	Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/shapes.scala	Sat Jan 03 20:22:27 2015 +0100
@@ -8,6 +8,8 @@
 package isabelle.graphview
 
 
+import isabelle._
+
 import java.awt.{BasicStroke, Graphics2D, Shape}
 import java.awt.geom.{AffineTransform, GeneralPath, Path2D, Rectangle2D, PathIterator}
 
@@ -16,8 +18,8 @@
 {
   trait Node
   {
-    def shape(m: Visualizer.Metrics, visualizer: Visualizer, peer: Option[String]): Shape
-    def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit
+    def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node): Shape
+    def paint(g: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node): Unit
   }
 
   object Growing_Node extends Node
@@ -25,24 +27,22 @@
     private val stroke =
       new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
 
-    def shape(m: Visualizer.Metrics, visualizer: Visualizer, peer: Option[String])
+    def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node)
       : Rectangle2D.Double =
     {
-      val (x, y) = visualizer.Coordinates(peer.get)
-      val bounds = m.string_bounds(visualizer.Caption(peer.get))
+      val (x, y) = visualizer.Coordinates(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)
     }
 
-    def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String])
+    def paint(g: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node)
     {
       val m = Visualizer.Metrics(g)
-      val s = shape(m, visualizer, peer)
-      val c = visualizer.node_color(peer)
-
-      val caption = visualizer.Caption(peer.get)
-      val bounds = m.string_bounds(caption)
+      val s = shape(m, visualizer, node)
+      val c = visualizer.node_color(node)
+      val bounds = m.string_bounds(node.toString)
 
       g.setColor(c.background)
       g.fill(s)
@@ -52,7 +52,7 @@
       g.draw(s)
 
       g.setColor(c.foreground)
-      g.drawString(caption,
+      g.drawString(node.toString,
         (s.getCenterX - bounds.getWidth / 2).round.toInt,
         (s.getCenterY - bounds.getHeight / 2 + m.ascent).round.toInt)
     }
@@ -64,22 +64,22 @@
       new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
     private val identity = new AffineTransform()
 
-    def shape(m: Visualizer.Metrics, visualizer: Visualizer, peer: Option[String]): Shape =
+    def shape(m: Visualizer.Metrics, visualizer: Visualizer, node: Graph_Display.Node): Shape =
     {
       val w = (m.space_width / 2).ceil
       new Rectangle2D.Double(- w, - w, 2 * w, 2 * w)
     }
 
-    def paint(g: Graphics2D, visualizer: Visualizer, peer: Option[String]): Unit =
-      paint_transformed(g, visualizer, peer, identity)
+    def paint(g: Graphics2D, visualizer: Visualizer, node: Graph_Display.Node): Unit =
+      paint_transformed(g, visualizer, node, identity)
 
     def paint_transformed(g: Graphics2D, visualizer: Visualizer,
-      peer: Option[String], at: AffineTransform)
+      node: Graph_Display.Node, at: AffineTransform)
     {
       val m = Visualizer.Metrics(g)
-      val s = shape(m, visualizer, peer)
+      val s = shape(m, visualizer, node)
+      val c = visualizer.node_color(node)
 
-      val c = visualizer.node_color(peer)
       g.setStroke(stroke)
       g.setColor(c.border)
       g.draw(at.createTransformedShape(s))
@@ -88,8 +88,8 @@
 
   trait Edge
   {
-    def paint(g: Graphics2D, visualizer: Visualizer,
-      peer: (String, String), head: Boolean, dummies: Boolean)
+    def paint(g: Graphics2D, visualizer: Visualizer, edge: Graph_Display.Edge,
+      head: Boolean, dummies: Boolean)
   }
 
   object Straight_Edge extends Edge
@@ -98,36 +98,37 @@
       new BasicStroke(1, BasicStroke.CAP_BUTT, BasicStroke.JOIN_ROUND)
 
     def paint(g: Graphics2D, visualizer: Visualizer,
-      peer: (String, String), head: Boolean, dummies: Boolean)
+      edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
     {
-      val ((fx, fy), (tx, ty)) = (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2))
+      val (fx, fy) = visualizer.Coordinates(edge._1)
+      val (tx, ty) = visualizer.Coordinates(edge._2)
       val ds =
       {
         val min = fy min ty
         val max = fy max ty
-        visualizer.Coordinates(peer).filter({ case (_, y) => y > min && y < max })
+        visualizer.Coordinates(edge).filter({ case (_, y) => min < y && y < max })
       }
       val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
 
       path.moveTo(fx, fy)
-      ds.foreach({case (x, y) => path.lineTo(x, y)})
+      ds.foreach({ case (x, y) => path.lineTo(x, y) })
       path.lineTo(tx, ty)
 
       if (dummies) {
         ds.foreach({
             case (x, y) => {
               val at = AffineTransform.getTranslateInstance(x, y)
-              Dummy.paint_transformed(g, visualizer, None, at)
+              Dummy.paint_transformed(g, visualizer, Graph_Display.Node.dummy, at)
             }
           })
       }
 
       g.setStroke(stroke)
-      g.setColor(visualizer.edge_color(peer))
+      g.setColor(visualizer.edge_color(edge))
       g.draw(path)
 
       if (head)
-        Arrow_Head.paint(g, path, visualizer.Drawer.shape(Visualizer.Metrics(g), Some(peer._2)))
+        Arrow_Head.paint(g, path, visualizer.Drawer.shape(Visualizer.Metrics(g), edge._2))
     }
   }
 
@@ -138,18 +139,18 @@
     private val slack = 0.1
 
     def paint(g: Graphics2D, visualizer: Visualizer,
-      peer: (String, String), head: Boolean, dummies: Boolean)
+      edge: Graph_Display.Edge, head: Boolean, dummies: Boolean)
     {
-      val ((fx, fy), (tx, ty)) =
-        (visualizer.Coordinates(peer._1), visualizer.Coordinates(peer._2))
+      val (fx, fy) = visualizer.Coordinates(edge._1)
+      val (tx, ty) = visualizer.Coordinates(edge._2)
       val ds =
       {
         val min = fy min ty
         val max = fy max ty
-        visualizer.Coordinates(peer).filter({case (_, y) => y > min && y < max})
+        visualizer.Coordinates(edge).filter({ case (_, y) => min < y && y < max })
       }
 
-      if (ds.isEmpty) Straight_Edge.paint(g, visualizer, peer, head, dummies)
+      if (ds.isEmpty) Straight_Edge.paint(g, visualizer, edge, head, dummies)
       else {
         val path = new GeneralPath(Path2D.WIND_EVEN_ODD, ds.length + 2)
         path.moveTo(fx, fy)
@@ -178,17 +179,17 @@
           ds.foreach({
               case (x, y) => {
                 val at = AffineTransform.getTranslateInstance(x, y)
-                Dummy.paint_transformed(g, visualizer, None, at)
+                Dummy.paint_transformed(g, visualizer, Graph_Display.Node.dummy, at)
               }
             })
         }
 
         g.setStroke(stroke)
-        g.setColor(visualizer.edge_color(peer))
+        g.setColor(visualizer.edge_color(edge))
         g.draw(path)
 
         if (head)
-          Arrow_Head.paint(g, path, visualizer.Drawer.shape(Visualizer.Metrics(g), Some(peer._2)))
+          Arrow_Head.paint(g, path, visualizer.Drawer.shape(Visualizer.Metrics(g), edge._2))
       }
     }
   }
@@ -202,7 +203,7 @@
       def intersecting_line(path: GeneralPath, shape: Shape): Option[(Point, Point)] =
       {
         val i = path.getPathIterator(null, 1.0)
-        val seg = Array[Double](0,0,0,0,0,0)
+        val seg = Array[Double](0.0, 0.0, 0.0, 0.0, 0.0, 0.0)
         var p1 = (0.0, 0.0)
         var p2 = (0.0, 0.0)
         while (!i.isDone()) {
diff -r 19b5fc4b2b38 -r be4180f3c236 src/Tools/Graphview/visualizer.scala
--- a/src/Tools/Graphview/visualizer.scala	Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/Graphview/visualizer.scala	Sat Jan 03 20:22:27 2015 +0100
@@ -105,21 +105,18 @@
   {
     private var layout = Layout.empty
 
-    def apply(k: String): (Double, Double) =
-      layout.nodes.getOrElse(k, (0.0, 0.0))
+    def apply(node: Graph_Display.Node): (Double, Double) =
+      layout.nodes.getOrElse(node, (0.0, 0.0))
 
-    def apply(e: (String, String)): List[(Double, Double)] =
-      layout.dummies.get(e) match {
-        case Some(ds) => ds
-        case None => Nil
-      }
+    def apply(edge: Graph_Display.Edge): List[(Double, Double)] =
+      layout.dummies.getOrElse(edge, Nil)
 
-    def reposition(k: String, to: (Double, Double))
+    def reposition(node: Graph_Display.Node, to: (Double, Double))
     {
-      layout = layout.copy(nodes = layout.nodes + (k -> to))
+      layout = layout.copy(nodes = layout.nodes + (node -> to))
     }
 
-    def reposition(d: ((String, String), Int), to: (Double, Double))
+    def reposition(d: (Graph_Display.Edge, Int), to: (Double, Double))
     {
       val (e, index) = d
       layout.dummies.get(e) match {
@@ -133,15 +130,15 @@
       }
     }
 
-    def translate(k: String, by: (Double, Double))
+    def translate(node: Graph_Display.Node, by: (Double, Double))
     {
-      val ((x, y), (dx, dy)) = (Coordinates(k), by)
-      reposition(k, (x + dx, y + dy))
+      val ((x, y), (dx, dy)) = (Coordinates(node), by)
+      reposition(node, (x + dx, y + dy))
     }
 
-    def translate(d: ((String, String), Int), by: (Double, Double))
+    def translate(d: (Graph_Display.Edge, Int), by: (Double, Double))
     {
-      val ((e, i),(dx, dy)) = (d, by)
+      val ((e, i), (dx, dy)) = (d, by)
       val (x, y) = apply(e)(i)
       reposition(d, (x + dx, y + dy))
     }
@@ -154,8 +151,8 @@
           val m = metrics()
 
           val max_width =
-            model.current_graph.iterator.map({ case (_, (info, _)) =>
-              m.string_bounds(info.name).getWidth }).max
+            model.current_graph.keys_iterator.map(
+              node => m.string_bounds(node.toString).getWidth).max
           val box_distance = (max_width + m.pad + m.gap).ceil
           def box_height(n: Int): Double = (m.char_width * 1.5 * (5 max n)).ceil
 
@@ -170,8 +167,8 @@
       var y0 = 0.0
       var x1 = 0.0
       var y1 = 0.0
-      for (node_name <- model.visible_nodes_iterator) {
-        val shape = Shapes.Growing_Node.shape(m, visualizer, Some(node_name))
+      for (node <- model.visible_nodes_iterator) {
+        val shape = Shapes.Growing_Node.shape(m, visualizer, node)
         x0 = x0 min shape.getMinX
         y0 = y0 min shape.getMinY
         x1 = x1 max shape.getMaxX
@@ -187,67 +184,46 @@
 
   object Drawer
   {
-    def apply(g: Graphics2D, n: Option[String])
-    {
-      n match {
-        case None =>
-        case Some(_) => Shapes.Growing_Node.paint(g, visualizer, n)
-      }
-    }
+    def apply(g: Graphics2D, node: Graph_Display.Node): Unit =
+      if (!node.is_dummy) Shapes.Growing_Node.paint(g, visualizer, node)
 
-    def apply(g: Graphics2D, e: (String, String), head: Boolean, dummies: Boolean)
-    {
-      Shapes.Cardinal_Spline_Edge.paint(g, visualizer, e, head, dummies)
-    }
+    def apply(g: Graphics2D, edge: Graph_Display.Edge, head: Boolean, dummies: Boolean): Unit =
+      Shapes.Cardinal_Spline_Edge.paint(g, visualizer, edge, head, dummies)
 
     def paint_all_visible(g: Graphics2D, dummies: Boolean)
     {
       g.setFont(font)
-
       g.setRenderingHints(rendering_hints)
-
-      model.visible_edges_iterator.foreach(e => {
-          apply(g, e, arrow_heads, dummies)
-        })
-
-      model.visible_nodes_iterator.foreach(l => {
-          apply(g, Some(l))
-        })
+      model.visible_edges_iterator.foreach(apply(g, _, arrow_heads, dummies))
+      model.visible_nodes_iterator.foreach(apply(g, _))
     }
 
-    def shape(m: Visualizer.Metrics, n: Option[String]): Shape =
-      if (n.isEmpty) Shapes.Dummy.shape(m, visualizer, n)
-      else Shapes.Growing_Node.shape(m, visualizer, n)
+    def shape(m: Visualizer.Metrics, node: Graph_Display.Node): Shape =
+      if (node.is_dummy) Shapes.Dummy.shape(m, visualizer, node)
+      else Shapes.Growing_Node.shape(m, visualizer, node)
   }
 
   object Selection
   {
-    private var selected: List[String] = Nil
+    // owned by GUI thread
+    private var state: List[Graph_Display.Node] = Nil
 
-    def apply() = selected
-    def apply(s: String) = selected.contains(s)
+    def get(): List[Graph_Display.Node] = GUI_Thread.require { state }
+    def contains(node: Graph_Display.Node): Boolean = get().contains(node)
 
-    def add(s: String) { selected = s :: selected }
-    def set(ss: List[String]) { selected = ss }
-    def clear() { selected = Nil }
+    def add(node: Graph_Display.Node): Unit = GUI_Thread.require { state = node :: state }
+    def clear(): Unit = GUI_Thread.require { state = Nil }
   }
 
   sealed case class Node_Color(border: Color, background: Color, foreground: Color)
 
-  def node_color(l: Option[String]): Node_Color =
-    l match {
-      case None =>
-        Node_Color(foreground1_color, background_color, foreground_color)
-      case Some(c) if Selection(c) =>
-        Node_Color(foreground_color, selection_color, foreground_color)
-      case Some(c) =>
-        Node_Color(foreground_color, model.colors.getOrElse(c, background_color), foreground_color)
-    }
+  def node_color(node: Graph_Display.Node): Node_Color =
+    if (node.is_dummy)
+      Node_Color(foreground1_color, background_color, foreground_color)
+    else if (Selection.contains(node))
+      Node_Color(foreground_color, selection_color, foreground_color)
+    else
+      Node_Color(foreground_color, model.colors.getOrElse(node, background_color), foreground_color)
 
-  def edge_color(e: (String, String)): Color = foreground_color
-
-  object Caption
-  {
-    def apply(key: String) = model.complete_graph.get_node(key).name
-  }
+  def edge_color(edge: Graph_Display.Edge): Color = foreground_color
 }
\ No newline at end of file
diff -r 19b5fc4b2b38 -r be4180f3c236 src/Tools/jEdit/src/active.scala
--- a/src/Tools/jEdit/src/active.scala	Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/jEdit/src/active.scala	Sat Jan 03 20:22:27 2015 +0100
@@ -41,10 +41,7 @@
               case XML.Elem(Markup(Markup.GRAPHVIEW, _), body) =>
                 Future.fork {
                   val graph =
-                    Exn.capture {
-                      isabelle.graphview.Model.decode_graph(body)
-                        .transitive_reduction_acyclic
-                    }
+                    Exn.capture { Graph_Display.decode_graph(body).transitive_reduction_acyclic }
                   GUI_Thread.later { Graphview_Dockable(view, snapshot, graph) }
                 }
 
diff -r 19b5fc4b2b38 -r be4180f3c236 src/Tools/jEdit/src/graphview_dockable.scala
--- a/src/Tools/jEdit/src/graphview_dockable.scala	Sat Jan 03 15:45:01 2015 +0100
+++ b/src/Tools/jEdit/src/graphview_dockable.scala	Sat Jan 03 20:22:27 2015 +0100
@@ -24,10 +24,10 @@
 
   private var implicit_snapshot = Document.Snapshot.init
 
-  private val no_graph: Exn.Result[graphview.Model.Graph] = Exn.Exn(ERROR("No graph"))
+  private val no_graph: Exn.Result[Graph_Display.Graph] = Exn.Exn(ERROR("No graph"))
   private var implicit_graph = no_graph
 
-  private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
+  private def set_implicit(snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph])
   {
     GUI_Thread.require {}
 
@@ -38,7 +38,7 @@
   private def reset_implicit(): Unit =
     set_implicit(Document.Snapshot.init, no_graph)
 
-  def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[graphview.Model.Graph])
+  def apply(view: View, snapshot: Document.Snapshot, graph: Exn.Result[Graph_Display.Graph])
   {
     set_implicit(snapshot, graph)
     view.getDockableWindowManager.floatDockableWindow("isabelle-graphview")