# HG changeset patch
# User wenzelm
# Date 1330274649 -3600
# Node ID c083a3f621c0a6c10b6c04ff4237d6c864a9a69c
# Parent  234f1730582d5471be003cbfe260783feace9895
more abstract class Document.Version;
tuned (NB: Version.nodes is total);

diff -r 234f1730582d -r c083a3f621c0 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Sun Feb 26 17:15:33 2012 +0100
+++ b/src/Pure/PIDE/document.scala	Sun Feb 26 17:44:09 2012 +0100
@@ -178,10 +178,12 @@
 
   object Version
   {
-    val init: Version = Version()
+    val init: Version = new Version()
+
+    def make(nodes: Nodes): Version = new Version(new_id(), nodes)
   }
 
-  sealed case class Version(
+  class Version private(
     val id: Version_ID = no_id,
     val nodes: Nodes = Map.empty.withDefaultValue(Node.empty))
   {
@@ -336,7 +338,8 @@
         case None => None
         case Some(st) =>
           val command = st.command
-          version.nodes.get(command.node_name).map((_, command))
+          val node = version.nodes(command.node_name)
+          Some((node, command))
       }
 
     def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
diff -r 234f1730582d -r c083a3f621c0 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Sun Feb 26 17:15:33 2012 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Feb 26 17:44:09 2012 +0100
@@ -145,7 +145,7 @@
   {
     val nodes = previous.nodes
     val (perspective, new_nodes) = update_perspective(nodes, name, text_perspective)
-    val version = Document.Version(Document.new_id(), new_nodes getOrElse nodes)
+    val version = Document.Version.make(new_nodes getOrElse nodes)
     (perspective, version)
   }
 
@@ -274,7 +274,7 @@
               nodes = nodes1
           }
       }
-      (doc_edits.toList, Document.Version(Document.new_id(), nodes))
+      (doc_edits.toList, Document.Version.make(nodes))
     }
   }
 }
diff -r 234f1730582d -r c083a3f621c0 src/Tools/jEdit/src/session_dockable.scala
--- a/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 17:15:33 2012 +0100
+++ b/src/Tools/jEdit/src/session_dockable.scala	Sun Feb 26 17:44:09 2012 +0100
@@ -146,14 +146,13 @@
   {
     Swing_Thread.now {
       val snapshot = Isabelle.session.snapshot()
-      val nodes = restriction getOrElse snapshot.version.nodes.keySet
+      val names = restriction getOrElse snapshot.version.nodes.keySet
 
-      var nodes_status1 = nodes_status
-      for {
-        name <- nodes
-        node <- snapshot.version.nodes.get(name)
-        val status = Protocol.node_status(snapshot.state, snapshot.version, node)
-      } nodes_status1 += (name -> status)
+      val nodes_status1 =
+        (nodes_status /: names)((status, name) => {
+          val node = snapshot.version.nodes(name)
+          status + (name -> Protocol.node_status(snapshot.state, snapshot.version, node))
+        })
 
       if (nodes_status != nodes_status1) {
         nodes_status = nodes_status1