src/Pure/PIDE/document.scala

--- a/src/Pure/PIDE/document.scala	Sun Aug 15 13:17:45 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Sun Aug 15 14:18:52 2010 +0200
@@ -78,9 +78,14 @@
   }
 
 
-  /* initial document */
+  /* document versions */
 
-  val init: Document = new Document(NO_ID, Map().withDefaultValue(Node.empty))
+  object Version
+  {
+    val init: Version = new Version(NO_ID, Map().withDefaultValue(Node.empty))
+  }
+
+  class Version(val id: Version_ID, val nodes: Map[String, Node])
 
 
 
@@ -94,8 +99,8 @@
 
   abstract class Snapshot
   {
-    val document: Document
-    val node: Document.Node
+    val version: Version
+    val node: Node
     val is_outdated: Boolean
     def convert(offset: Int): Int
     def revert(offset: Int): Int
@@ -105,16 +110,16 @@
 
   object Change
   {
-    val init = new Change(Future.value(Document.init), Nil, Future.value(Nil, Document.init))
+    val init = new Change(Future.value(Version.init), Nil, Future.value(Nil, Version.init))
   }
 
   class Change(
-    val prev: Future[Document],
+    val previous: Future[Version],
     val edits: List[Node_Text_Edit],
-    val result: Future[(List[Edit[Command]], Document)])
+    val result: Future[(List[Edit[Command]], Version)])
   {
-    val document: Future[Document] = result.map(_._2)
-    def is_finished: Boolean = prev.is_finished && document.is_finished
+    val current: Future[Version] = result.map(_._2)
+    def is_finished: Boolean = previous.is_finished && current.is_finished
   }
 
 
@@ -125,7 +130,7 @@
   {
     class Fail(state: State) extends Exception
 
-    val init = State().define_document(Document.init, Map()).assign(Document.init.id, Nil)
+    val init = State().define_version(Version.init, Map()).assign(Version.init.id, Nil)
 
     class Assignment(former_assignment: Map[Command, Exec_ID])
     {
@@ -142,20 +147,20 @@
   }
 
   case class State(
-    val documents: Map[Version_ID, Document] = Map(),
+    val versions: Map[Version_ID, Version] = Map(),
     val commands: Map[Command_ID, Command.State] = Map(),
-    val execs: Map[Exec_ID, (Command.State, Set[Document])] = Map(),
-    val assignments: Map[Document, State.Assignment] = Map(),
+    val execs: Map[Exec_ID, (Command.State, Set[Version])] = Map(),
+    val assignments: Map[Version, State.Assignment] = Map(),
     val disposed: Set[ID] = Set())  // FIXME unused!?
   {
     private def fail[A]: A = throw new State.Fail(this)
 
-    def define_document(document: Document, former_assignment: Map[Command, Exec_ID]): State =
+    def define_version(version: Version, former_assignment: Map[Command, Exec_ID]): State =
     {
-      val id = document.id
-      if (documents.isDefinedAt(id) || disposed(id)) fail
-      copy(documents = documents + (id -> document),
-        assignments = assignments + (document -> new State.Assignment(former_assignment)))
+      val id = version.id
+      if (versions.isDefinedAt(id) || disposed(id)) fail
+      copy(versions = versions + (id -> version),
+        assignments = assignments + (version -> new State.Assignment(former_assignment)))
     }
 
     def define_command(command: Command): State =
@@ -167,16 +172,16 @@
 
     def lookup_command(id: Command_ID): Option[Command] = commands.get(id).map(_.command)
 
-    def the_document(id: Version_ID): Document = documents.getOrElse(id, fail)
+    def the_version(id: Version_ID): Version = versions.getOrElse(id, fail)
     def the_command(id: Command_ID): Command.State = commands.getOrElse(id, fail)
     def the_exec_state(id: Exec_ID): Command.State = execs.getOrElse(id, fail)._1
-    def the_assignment(document: Document): State.Assignment = assignments.getOrElse(document, fail)
+    def the_assignment(version: Version): State.Assignment = assignments.getOrElse(version, fail)
 
     def accumulate(id: ID, message: XML.Tree): (Command.State, State) =
       execs.get(id) match {
-        case Some((st, docs)) =>
+        case Some((st, occs)) =>
           val new_st = st.accumulate(message)
-          (new_st, copy(execs = execs + (id -> (new_st, docs))))
+          (new_st, copy(execs = execs + (id -> (new_st, occs))))
         case None =>
           commands.get(id) match {
             case Some(st) =>
@@ -188,38 +193,33 @@
 
     def assign(id: Version_ID, edits: List[(Command_ID, Exec_ID)]): State =
     {
-      val doc = the_document(id)
-      val docs = Set(doc)  // FIXME unused (!?)
+      val version = the_version(id)
+      val occs = Set(version)  // FIXME unused (!?)
 
       var new_execs = execs
       val assigned_execs =
         for ((cmd_id, exec_id) <- edits) yield {
           val st = the_command(cmd_id)
           if (new_execs.isDefinedAt(exec_id) || disposed(exec_id)) fail
-          new_execs += (exec_id -> (st, docs))
+          new_execs += (exec_id -> (st, occs))
           (st.command, exec_id)
         }
-      the_assignment(doc).assign(assigned_execs)  // FIXME explicit value instead of promise (!?)
+      the_assignment(version).assign(assigned_execs)  // FIXME explicit value instead of promise (!?)
       copy(execs = new_execs)
     }
 
-    def is_assigned(document: Document): Boolean =
-      assignments.get(document) match {
+    def is_assigned(version: Version): Boolean =
+      assignments.get(version) match {
         case Some(assgn) => assgn.is_finished
         case None => false
       }
 
-    def command_state(document: Document, command: Command): Command.State =
+    def command_state(version: Version, command: Command): Command.State =
     {
-      val assgn = the_assignment(document)
+      val assgn = the_assignment(version)
       require(assgn.is_finished)
       the_exec_state(assgn.join.getOrElse(command, fail))
     }
   }
 }
 
-
-class Document(
-    val id: Document.Version_ID,
-    val nodes: Map[String, Document.Node])
-