src/Pure/System/session.scala

--- a/src/Pure/System/session.scala	Sun Aug 15 13:17:45 2010 +0200
+++ b/src/Pure/System/session.scala	Sun Aug 15 14:18:52 2010 +0200
@@ -81,14 +81,14 @@
     {
       require(change.is_finished)
 
-      val old_doc = change.prev.join
-      val (node_edits, doc) = change.result.join
+      val previous = change.previous.join
+      val (node_edits, current) = change.result.join
 
-      var former_assignment = current_state().the_assignment(old_doc).join
+      var former_assignment = current_state().the_assignment(previous).join
       for {
         (name, Some(cmd_edits)) <- node_edits
         (prev, None) <- cmd_edits
-        removed <- old_doc.nodes(name).commands.get_after(prev)
+        removed <- previous.nodes(name).commands.get_after(prev)
       } former_assignment -= removed
 
       val id_edits =
@@ -113,8 +113,8 @@
               }
             (name -> Some(ids))
         }
-      change_state(_.define_document(doc, former_assignment))
-      prover.edit_document(old_doc.id, doc.id, id_edits)
+      change_state(_.define_version(current, former_assignment))
+      prover.edit_version(previous.id, current.id, id_edits)
     }
     //}}}
 
@@ -142,8 +142,8 @@
         case None =>
           if (result.is_status) {
             result.body match {
-              case List(Isar_Document.Assign(doc_id, edits)) =>
-                try { change_state(_.assign(doc_id, edits)) }
+              case List(Isar_Document.Assign(id, edits)) =>
+                try { change_state(_.assign(id, edits)) }
                 catch { case _: Document.State.Fail => bad_result(result) }
               case List(Keyword.Command_Decl(name, kind)) => syntax += (name, kind)
               case List(Keyword.Keyword_Decl(name)) => syntax += name
@@ -286,7 +286,7 @@
 
   /** editor history **/
 
-  private case class Edit_Document(edits: List[Document.Node_Text_Edit])
+  private case class Edit_Version(edits: List[Document.Node_Text_Edit])
 
   private val editor_history = new Actor
   {
@@ -298,7 +298,7 @@
       val history_snapshot = history
 
       val found_stable = history_snapshot.find(change =>
-        change.is_finished && state_snapshot.is_assigned(change.document.join))
+        change.is_finished && state_snapshot.is_assigned(change.current.join))
       require(found_stable.isDefined)
       val stable = found_stable.get
       val latest = history_snapshot.head
@@ -309,15 +309,15 @@
       lazy val reverse_edits = edits.reverse
 
       new Document.Snapshot {
-        val document = stable.document.join
-        val node = document.nodes(name)
+        val version = stable.current.join
+        val node = version.nodes(name)
         val is_outdated = !(pending_edits.isEmpty && latest == stable)
         def convert(offset: Int): Int = (offset /: edits)((i, edit) => edit.convert(i))
         def revert(offset: Int): Int = (offset /: reverse_edits)((i, edit) => edit.revert(i))
         def lookup_command(id: Document.Command_ID): Option[Command] =
           state_snapshot.lookup_command(id)
         def state(command: Command): Command.State =
-          try { state_snapshot.command_state(document, command) }
+          try { state_snapshot.command_state(version, command) }
           catch { case _: Document.State.Fail => command.empty_state }
       }
     }
@@ -326,20 +326,20 @@
     {
       loop {
         react {
-          case Edit_Document(edits) =>
+          case Edit_Version(edits) =>
             val history_snapshot = history
             require(!history_snapshot.isEmpty)
 
-            val prev = history_snapshot.head.document
-            val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
+            val prev = history_snapshot.head.current
+            val result =
               isabelle.Future.fork {
-                val old_doc = prev.join
-                val former_assignment = current_state().the_assignment(old_doc).join  // FIXME async!?
-                Thy_Syntax.text_edits(Session.this, old_doc, edits)
+                val previous = prev.join
+                val former_assignment = current_state().the_assignment(previous).join  // FIXME async!?
+                Thy_Syntax.text_edits(Session.this, previous, edits)
               }
             val new_change = new Document.Change(prev, edits, result)
             history ::= new_change
-            new_change.document.map(_ => session_actor ! new_change)
+            new_change.current.map(_ => session_actor ! new_change)
             reply(())
 
           case bad => System.err.println("editor_model: ignoring bad message " + bad)
@@ -361,5 +361,5 @@
   def snapshot(name: String, pending_edits: List[Text_Edit]): Document.Snapshot =
     editor_history.snapshot(name, pending_edits)
 
-  def edit_document(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Document(edits) }
+  def edit_version(edits: List[Document.Node_Text_Edit]) { editor_history !? Edit_Version(edits) }
 }