graph traversal in topological order;
Session.snapshot() with sensible defaults;

--- a/src/Pure/PIDE/document.scala	Sat Sep 17 23:04:03 2011 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Sep 18 00:05:22 2011 +0200
@@ -173,6 +173,20 @@
 
   type Nodes = Map[Node.Name, Node]
   sealed case class Version(val id: Version_ID, val nodes: Nodes)
+  {
+    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,
+        Library.sort_wrt((name: Node.Name) => name.node, nodes.keys.toList))
+    }
+  }
 
 
   /* changes of plain text, eventually resulting in document edits */

--- a/src/Pure/System/session.scala	Sat Sep 17 23:04:03 2011 +0200
+++ b/src/Pure/System/session.scala	Sun Sep 18 00:05:22 2011 +0200
@@ -107,7 +107,8 @@
   private val global_state = new Volatile(Document.State.init)
   def current_state(): Document.State = global_state()
 
-  def snapshot(name: Document.Node.Name, pending_edits: List[Text.Edit]): Document.Snapshot =
+  def snapshot(name: Document.Node.Name = Document.Node.Name.empty,
+      pending_edits: List[Text.Edit] = Nil): Document.Snapshot =
     global_state().snapshot(name, pending_edits)
 
 

--- a/src/Pure/library.scala	Sat Sep 17 23:04:03 2011 +0200
+++ b/src/Pure/library.scala	Sun Sep 18 00:05:22 2011 +0200
@@ -139,6 +139,26 @@
   }
 
 
+  /* 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)

--- a/src/Tools/jEdit/src/session_dockable.scala	Sat Sep 17 23:04:03 2011 +0200
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Sep 18 00:05:22 2011 +0200
@@ -138,20 +138,20 @@
   {
     Swing_Thread.now {
       // FIXME correlation to changed_nodes!?
-      val state = Isabelle.session.current_state()
-      val version = state.recent_stable.version.get_finished
+      val snapshot = Isabelle.session.snapshot()
 
       var nodes_status1 = nodes_status
       for {
         name <- changed_nodes
-        node <- version.nodes.get(name)
-        val status = Isar_Document.node_status(state, version, node)
+        node <- snapshot.version.nodes.get(name)
+        val status = Isar_Document.node_status(snapshot.state, snapshot.version, node)
       } nodes_status1 += (name -> status)
 
       if (nodes_status != nodes_status1) {
         nodes_status = nodes_status1
         status.listData =
-          Library.sort_wrt((name: Document.Node.Name) => name.node, nodes_status.keySet.toList)
+          snapshot.version.topological_order.filter(
+            (name: Document.Node.Name) => nodes_status.isDefinedAt(name))
       }
     }
   }