# HG changeset patch
# User wenzelm
# Date 1281621704 -7200
# Node ID 827b90f18ff424b340816b3d5ab58d03603b4a55
# Parent  af7f41a8a0a8b462d59ac3814c400be4d3aee679
Change: eliminated id, which is merely the resulting document id and is only required in joined state anyway;
Document.edit_text: create new document id here;

diff -r af7f41a8a0a8 -r 827b90f18ff4 src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Thu Aug 12 15:19:11 2010 +0200
+++ b/src/Pure/PIDE/document.scala	Thu Aug 12 16:01:44 2010 +0200
@@ -107,11 +107,10 @@
 
   object Change
   {
-    val init = new Change(NO_ID, None, Nil, Future.value(Nil, Document.init))
+    val init = new Change(None, Nil, Future.value(Nil, Document.init))
   }
 
   class Change(
-    val id: Version_ID,
     val parent: Option[Change],
     val edits: List[Node_Text_Edit],
     val result: Future[(List[Edit[Command]], Document)])
@@ -156,8 +155,8 @@
 
   /** editing **/
 
-  def text_edits(session: Session, old_doc: Document, new_id: Version_ID,
-      edits: List[Node_Text_Edit]): (List[Edit[Command]], Document) =
+  def text_edits(session: Session, old_doc: Document, edits: List[Node_Text_Edit])
+      : (List[Edit[Command]], Document) =
   {
     require(old_doc.assignment.is_finished)
 
@@ -258,7 +257,7 @@
         nodes += (name -> new Node(commands2))
         former_assignment --= removed_commands
       }
-      (doc_edits.toList, new Document(new_id, nodes, former_assignment))
+      (doc_edits.toList, new Document(session.create_id(), nodes, former_assignment))
     }
   }
 }
diff -r af7f41a8a0a8 -r 827b90f18ff4 src/Pure/System/session.scala
--- a/src/Pure/System/session.scala	Thu Aug 12 15:19:11 2010 +0200
+++ b/src/Pure/System/session.scala	Thu Aug 12 16:01:44 2010 +0200
@@ -125,7 +125,7 @@
             (name -> Some(chs))
         }
       register_document(doc)
-      prover.edit_document(change.parent.get.id, doc.id, id_edits)
+      prover.edit_document(change.parent.get.join_document.id, doc.id, id_edits)
     }
     //}}}
 
@@ -328,14 +328,13 @@
         react {
           case Edit_Document(edits) =>
             val old_change = history
-            val new_id = create_id()
             val result: isabelle.Future[(List[Document.Edit[Command]], Document)] =
               isabelle.Future.fork {
                 val old_doc = old_change.join_document
                 old_doc.await_assignment
-                Document.text_edits(Session.this, old_doc, new_id, edits)
+                Document.text_edits(Session.this, old_doc, edits)
               }
-            val new_change = new Document.Change(new_id, Some(old_change), edits, result)
+            val new_change = new Document.Change(Some(old_change), edits, result)
             history = new_change
             new_change.result.map(_ => session_actor ! new_change)
             reply(())