renamed class Document to Document.Version etc.;
renamed Change.prev to Change.previous, and Change.document to Change.current;
tuned;

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

--- a/src/Pure/System/isar_document.ML	Sun Aug 15 13:17:45 2010 +0200
+++ b/src/Pure/System/isar_document.ML	Sun Aug 15 14:18:52 2010 +0200
@@ -27,11 +27,11 @@
 fun err_undef kind id = error ("Undefined " ^ kind ^ ": " ^ Document.print_id id);
 
 
-(** documents **)
+(** document versions **)
 
 datatype entry = Entry of {next: Document.command_id option, exec: Document.exec_id option};
 type node = entry Inttab.table; (*unique command entries indexed by command_id, start with no_id*)
-type document = node Graph.T;   (*development graph via static imports*)
+type version = node Graph.T;   (*development graph via static imports*)
 
 
 (* command entries *)
@@ -97,8 +97,8 @@
 
 val empty_node: node = Inttab.make [(Document.no_id, make_entry NONE (SOME Document.no_id))];
 
-fun the_node (document: document) name =
-  Graph.get_node document name handle Graph.UNDEF _ => empty_node;
+fun the_node (version: version) name =
+  Graph.get_node version name handle Graph.UNDEF _ => empty_node;
 
 fun edit_node (id, SOME id2) = insert_after id id2
   | edit_node (id, NONE) = delete_after id;
@@ -166,19 +166,19 @@
 
 local
 
-val global_documents = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: document)]);
+val global_versions = Unsynchronized.ref (Inttab.make [(Document.no_id, Graph.empty: version)]);
 
 in
 
-fun define_document (id: Document.version_id) document =
+fun define_version (id: Document.version_id) version =
   NAMED_CRITICAL "Isar" (fn () =>
-    Unsynchronized.change global_documents (Inttab.update_new (id, document))
-      handle Inttab.DUP dup => err_dup "document" dup);
+    Unsynchronized.change global_versions (Inttab.update_new (id, version))
+      handle Inttab.DUP dup => err_dup "version" dup);
 
-fun the_document (id: Document.version_id) =
-  (case Inttab.lookup (! global_documents) id of
-    NONE => err_undef "document" id
-  | SOME document => document);
+fun the_version (id: Document.version_id) =
+  (case Inttab.lookup (! global_versions) id of
+    NONE => err_undef "version" id
+  | SOME version => version);
 
 end;
 
@@ -197,20 +197,20 @@
 
 in
 
-fun execute document =
+fun execute version =
   NAMED_CRITICAL "Isar" (fn () =>
     let
       val old_execution = ! execution;
       val _ = List.app Future.cancel old_execution;
       fun await_cancellation () = uninterruptible (K Future.join_results) old_execution;
       (* FIXME proper node deps *)
-      val new_execution = Graph.keys document |> map (fn name =>
+      val new_execution = Graph.keys version |> map (fn name =>
         Future.fork_pri 1 (fn () =>
           let
             val _ = await_cancellation ();
             val exec =
               fold_entries Document.no_id (fn (_, {exec, ...}) => fn () => force_exec exec)
-                (the_node document name);
+                (the_node version name);
           in exec () end));
     in execution := new_execution end);
 
@@ -249,11 +249,11 @@
 fun edit_document (old_id: Document.version_id) (new_id: Document.version_id) edits =
   NAMED_CRITICAL "Isar" (fn () =>
     let
-      val old_document = the_document old_id;
-      val new_document = fold edit_nodes edits old_document;
+      val old_version = the_version old_id;
+      val new_version = fold edit_nodes edits old_version;
 
       fun update_node name node =
-        (case first_entry (is_changed (the_node old_document name)) node of
+        (case first_entry (is_changed (the_node old_version name)) node of
           NONE => ([], node)
         | SOME (prev, id, _) =>
             let
@@ -263,13 +263,13 @@
             in (rev updates, node') end);
 
       (* FIXME proper node deps *)
-      val (updatess, new_document') =
-        (Graph.keys new_document, new_document)
+      val (updatess, new_version') =
+        (Graph.keys new_version, new_version)
           |-> fold_map (fn name => Graph.map_node_yield name (update_node name));
 
-      val _ = define_document new_id new_document';
+      val _ = define_version new_id new_version';
       val _ = updates_status new_id (flat updatess);
-      val _ = execute new_document';
+      val _ = execute new_version';
     in () end);
 
 end;
@@ -283,7 +283,7 @@
     (fn [id, text] => define_command (Document.parse_id id) text);
 
 val _ =
-  Isabelle_Process.add_command "Isar_Document.edit_document"
+  Isabelle_Process.add_command "Isar_Document.edit_version"
     (fn [old_id, new_id, edits] =>
       edit_document (Document.parse_id old_id) (Document.parse_id new_id)
         (XML_Data.dest_list (XML_Data.dest_pair XML_Data.dest_string

--- a/src/Pure/System/isar_document.scala	Sun Aug 15 13:17:45 2010 +0200
+++ b/src/Pure/System/isar_document.scala	Sun Aug 15 14:18:52 2010 +0200
@@ -46,9 +46,9 @@
     input("Isar_Document.define_command", Document.ID(id), text)
 
 
-  /* documents */
+  /* document versions */
 
-  def edit_document(old_id: Document.Version_ID, new_id: Document.Version_ID,
+  def edit_version(old_id: Document.Version_ID, new_id: Document.Version_ID,
       edits: List[Document.Edit[Document.Command_ID]])
   {
     def make_id1(id1: Option[Document.Command_ID]): XML.Body =
@@ -60,7 +60,7 @@
           XML_Data.make_option(XML_Data.make_list(
               XML_Data.make_pair(make_id1)(XML_Data.make_option(XML_Data.make_long))))))(edits)
 
-    input("Isar_Document.edit_document",
+    input("Isar_Document.edit_version",
       Document.ID(old_id), Document.ID(new_id), YXML.string_of_body(arg))
   }
 }

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

--- a/src/Pure/Thy/thy_syntax.scala	Sun Aug 15 13:17:45 2010 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Sun Aug 15 14:18:52 2010 +0200
@@ -38,8 +38,8 @@
 
   /** text edits **/
 
-  def text_edits(session: Session, old_doc: Document, edits: List[Document.Node_Text_Edit])
-      : (List[Document.Edit[Command]], Document) =
+  def text_edits(session: Session, previous: Document.Version,
+      edits: List[Document.Node_Text_Edit]): (List[Document.Edit[Command]], Document.Version) =
   {
     /* phase 1: edit individual command source */
 
@@ -110,7 +110,7 @@
 
     {
       val doc_edits = new mutable.ListBuffer[Document.Edit[Command]]
-      var nodes = old_doc.nodes
+      var nodes = previous.nodes
 
       for ((name, text_edits) <- edits) {
         val commands0 = nodes(name).commands
@@ -127,7 +127,7 @@
         doc_edits += (name -> Some(cmd_edits))
         nodes += (name -> new Document.Node(commands2))
       }
-      (doc_edits.toList, new Document(session.create_id(), nodes))
+      (doc_edits.toList, new Document.Version(session.create_id(), nodes))
     }
   }
 }

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 13:17:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Aug 15 14:18:52 2010 +0200
@@ -203,7 +203,7 @@
     def snapshot(): List[Text_Edit] = pending.toList
 
     private val delay_flush = Swing_Thread.delay_last(session.input_delay) {
-      if (!pending.isEmpty) session.edit_document(List((thy_name, flush())))
+      if (!pending.isEmpty) session.edit_version(List((thy_name, flush())))
     }
 
     def flush(): List[Text_Edit] =
@@ -225,7 +225,8 @@
 
   /* snapshot */
 
-  def snapshot(): Document.Snapshot = {
+  def snapshot(): Document.Snapshot =
+  {
     Swing_Thread.require()
     session.snapshot(thy_name, pending_edits.snapshot())
   }

--- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Aug 15 13:17:45 2010 +0200
+++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala	Sun Aug 15 14:18:52 2010 +0200
@@ -95,9 +95,9 @@
     import Isabelle_Sidekick.int_to_pos
 
     val root = data.root
-    val doc = Swing_Thread.now { model.snapshot().node }  // FIXME cover all nodes (!??)
+    val snapshot = Swing_Thread.now { model.snapshot() }  // FIXME cover all nodes (!??)
     for {
-      (command, command_start) <- doc.command_range(0)
+      (command, command_start) <- snapshot.node.command_range(0)
       if command.is_command && !stopped
     }
     {
@@ -113,8 +113,7 @@
           override def getStart: Position = command_start
           override def setEnd(end: Position) = ()
           override def getEnd: Position = command_start + command.length
-          override def toString = name
-        })
+          override def toString = name})
       root.add(node)
     }
   }