src/Pure/PIDE/document.scala

 
   type Nodes = Map[Node.Name, Node]
 
   object Version
   {
-    val init: Version = Version()
-  }
-
-  sealed case class Version(
+    val init: Version = new Version()
+
+    def make(nodes: Nodes): Version = new Version(new_id(), nodes)
+  }
+
+  class Version private(
     val id: Version_ID = no_id,
     val nodes: Nodes = Map.empty.withDefaultValue(Node.empty))
   {
     def topological_order: List[Node.Name] =
     {

     def find_command(version: Version, id: ID): Option[(Node, Command)] =
       commands.get(id) orElse execs.get(id) match {
         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)
     def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)  // FIXME rename
     def the_exec(id: Exec_ID): Command.State = execs.getOrElse(id, fail)