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