# HG changeset patch
# User wenzelm
# Date 1330382111 -3600
# Node ID 54ea872b60eaee2f9334b153683c47d0b02ea2b6
# Parent  d0491ab69c84bd61353ea42782a90d7ec79e81e0
more explicit development graph;

diff -r d0491ab69c84 -r 54ea872b60ea src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Mon Feb 27 23:30:38 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Mon Feb 27 23:35:11 2012 +0100
@@ -29,7 +29,7 @@
 
   /** document structure **/
 
-  /* named nodes -- development graph */
+  /* individual nodes */
 
   type Edit[A, B] = (Node.Name, Node.Edit[A, B])
   type Edit_Text = Edit[Text.Edit, Text.Perspective]
@@ -49,6 +49,11 @@
         val theory = Thy_Header.thy_name(node) getOrElse error("Bad theory file name: " + path)
         Name(node, dir, theory)
       }
+
+      object Ordering extends scala.math.Ordering[Name]
+      {
+        def compare(name1: Name, name2: Name): Int = name1.node compare name2.node
+      }
     }
     sealed case class Name(node: String, dir: String, theory: String)
     {
@@ -169,13 +174,50 @@
   }
 
 
+  /* development graph */
+
+  object Nodes
+  {
+    val empty: Nodes = new Nodes(Graph.empty(Node.Name.Ordering))
+  }
+
+  final class Nodes private(graph: Graph[Node.Name, Node])
+  {
+    def get_name(s: String): Option[Node.Name] =
+      graph.keys.find(name => name.node == s)
+
+    def apply(name: Node.Name): Node =
+      graph.default_node(name, Node.empty).get_node(name)
+
+    def + (entry: (Node.Name, Node)): Nodes =
+    {
+      val (name, node) = entry
+      val parents =
+        node.header match {
+          case Exn.Res(header) =>
+            // FIXME official names of yet unknown nodes!?
+            for (imp <- header.imports; imp_name <- get_name(imp)) yield imp_name
+          case _ => Nil
+        }
+      val graph1 =
+        (graph.default_node(name, Node.empty) /: parents)((g, p) => g.default_node(p, Node.empty))
+      val graph2 = (graph1 /: graph1.imm_preds(name))((g, dep) => g.del_edge(dep, name))
+      val graph3 = (graph2 /: parents)((g, dep) => g.add_edge(dep, name))
+      new Nodes(graph3.map_node(name, _ => node))
+    }
+
+    def entries: Iterator[(Node.Name, Node)] =
+      graph.entries.map({ case (name, (node, _)) => (name, node) })
+
+    def topological_order: List[Node.Name] = graph.topological_order
+  }
+
+
 
   /** versioning **/
 
   /* particular document versions */
 
-  type Nodes = Map[Node.Name, Node]
-
   object Version
   {
     val init: Version = new Version()
@@ -185,20 +227,7 @@
 
   final class Version private(
     val id: Version_ID = no_id,
-    val nodes: Nodes = Map.empty.withDefaultValue(Node.empty))
-  {
-    def topological_order: List[Node.Name] =
-    {
-      val names = nodes.map({ case (name, node) => (name.node -> name) })
-      def next(x: Node.Name): List[Node.Name] =
-        nodes(x).header match {
-          case Exn.Res(header) =>
-            for (imp <- header.imports; name <- names.get(imp)) yield(name)
-          case Exn.Exn(_) => Nil
-        }
-      Library.topological_order(next, nodes.keys.toList.sortBy(_.node))
-    }
-  }
+    val nodes: Nodes = Nodes.empty)
 
 
   /* changes of plain text, eventually resulting in document edits */
@@ -440,7 +469,7 @@
       for {
         (version_id, version) <- versions1.iterator
         val command_execs = assignments1(version_id).command_execs
-        (_, node) <- version.nodes.iterator
+        (_, node) <- version.nodes.entries
         command <- node.commands.iterator
       } {
         val id = command.id
diff -r d0491ab69c84 -r 54ea872b60ea src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Feb 27 23:30:38 2012 +0100
+++ b/src/Pure/library.scala	Mon Feb 27 23:35:11 2012 +0100
@@ -128,26 +128,6 @@
   }
 
 
-  /* graph traversal */
-
-  def topological_order[A](next: A => Iterable[A], starts: Iterable[A]): List[A] =
-  {
-    type Reached = (List[A], Set[A])
-    def reach(reached: Reached, x: A): Reached =
-    {
-      val (rs, r_set) = reached
-      if (r_set(x)) reached
-      else {
-        val (rs1, r_set1) = reachs((rs, r_set + x), next(x))
-        (x :: rs1, r_set1)
-      }
-    }
-    def reachs(reached: Reached, xs: Iterable[A]): Reached = (reached /: xs)(reach)
-
-    reachs((Nil, Set.empty), starts)._1.reverse
-  }
-
-
   /* simple dialogs */
 
   private def simple_dialog(kind: Int, default_title: String)
diff -r d0491ab69c84 -r 54ea872b60ea src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Mon Feb 27 23:30:38 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala	Mon Feb 27 23:35:11 2012 +0100
@@ -147,18 +147,20 @@
   {
     Swing_Thread.now {
       val snapshot = Isabelle.session.snapshot()
-      val names = restriction getOrElse snapshot.version.nodes.keySet
 
+      val iterator =
+        restriction match {
+          case Some(names) => names.iterator.map(name => (name, snapshot.version.nodes(name)))
+          case None => snapshot.version.nodes.entries
+        }
       val nodes_status1 =
-        (nodes_status /: names)((status, name) => {
-          val node = snapshot.version.nodes(name)
-          status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node))
-        })
+        (nodes_status /: iterator)({ case (status, (name, node)) =>
+            status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node)) })
 
       if (nodes_status != nodes_status1) {
         nodes_status = nodes_status1
         status.listData =
-          snapshot.version.topological_order.filter(
+          snapshot.version.nodes.topological_order.filter(
             (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
       }
     }