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