# HG changeset patch
# User wenzelm
# Date 1263138021 -3600
# Node ID 32b49207ca207730246d3be00d84c6ff16ce01a5
# Parent  d21c997104c4f53fd36df2e2463b4de7324386d7
misc tuning and clarification of Document/Change;

diff -r d21c997104c4 -r 32b49207ca20 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Sun Jan 10 15:42:31 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Sun Jan 10 16:40:21 2010 +0100
@@ -61,16 +61,16 @@
   private val document_0 = session.begin_document(buffer.getName)
 
   @volatile private var history =  // owned by Swing thread
-    new Change(None, Nil, document_0.id, Future.value(document_0, Nil))
+    new Change(document_0.id, None, Nil, Future.value(Nil, document_0))
 
   def current_change(): Change = history
 
   def recent_document(): Document =
   {
     def find(change: Change): Change =
-      if (change.result.is_finished && change.document.assignment.is_finished) change
+      if (change.result.is_finished && change.join_document.assignment.is_finished) change
       else find(change.parent.get)
-    find(current_change()).document
+    find(current_change()).join_document
   }
 
 
@@ -102,16 +102,10 @@
 
   private val edits_delay = Swing_Thread.delay_last(300) {
     if (!edits_buffer.isEmpty) {
-      val edits = edits_buffer.toList
-      val change1 = current_change()
-      val result_id = session.create_id()
-      val result: Future[Document.Result] = Future.fork {
-        Document.text_edits(session, change1.document, result_id, edits)
-      }
-      val change2 = new Change(Some(change1), edits, result_id, result)
-      history = change2
-      result.map(_ => session.input(change2))
+      val new_change = current_change().edit(session, edits_buffer.toList)
       edits_buffer.clear
+      history = new_change
+      new_change.result.map(_ => session.input(new_change))
     }
   }
 
diff -r d21c997104c4 -r 32b49207ca20 src/Tools/jEdit/src/proofdocument/change.scala
--- a/src/Tools/jEdit/src/proofdocument/change.scala	Sun Jan 10 15:42:31 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/change.scala	Sun Jan 10 16:40:21 2010 +0100
@@ -9,10 +9,10 @@
 
 
 class Change(
+  val id: Isar_Document.Document_ID,
   val parent: Option[Change],
   val edits: List[Text_Edit],
-  val id: Isar_Document.Document_ID,
-  val result: Future[Document.Result])
+  val result: Future[(List[Document.Edit], Document)])
 {
   def ancestors: Iterator[Change] = new Iterator[Change]
   {
@@ -25,6 +25,17 @@
       }
   }
 
-  def document: Document = result.join._1
-  def document_edits: List[Document.Structure_Edit] = result.join._2
+  def join_document: Document = result.join._2
+
+  def edit(session: Session, edits: List[Text_Edit]): Change =
+  {
+    val new_id = session.create_id()
+    val result: Future[(List[Document.Edit], Document)] =
+      Future.fork {
+        val old_doc = join_document
+        old_doc.await_assignment
+        Document.text_edits(session, old_doc, new_id, edits)
+      }
+    new Change(new_id, Some(this), edits, result)
+  }
 }
\ No newline at end of file
diff -r d21c997104c4 -r 32b49207ca20 src/Tools/jEdit/src/proofdocument/document.scala
--- a/src/Tools/jEdit/src/proofdocument/document.scala	Sun Jan 10 15:42:31 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/document.scala	Sun Jan 10 16:40:21 2010 +0100
@@ -40,18 +40,16 @@
     doc
   }
 
-  type Structure_Edit = (Option[Command], Option[Command])
-  type Structure_Change = List[Structure_Edit]
-  type Result = (Document, List[Structure_Edit])
+  type Edit = (Option[Command], Option[Command])
 
   def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
-    edits: List[Text_Edit]): Result =
+    edits: List[Text_Edit]): (List[Edit], Document) =
   {
     require(old_doc.assignment.is_finished)
     val doc0 =
       Document_Body(old_doc.tokens, old_doc.token_start, old_doc.commands, old_doc.assignment.join)
 
-    val changes = new mutable.ListBuffer[Structure_Edit]
+    val changes = new mutable.ListBuffer[Edit]
     val doc = (doc0 /: edits)((doc1: Document_Body, edit: Text_Edit) =>
       {
         val (doc2, chgs) = doc1.text_edit(session, edit)
@@ -59,7 +57,7 @@
         doc2
       })
     val new_doc = new Document(new_id, doc.tokens, doc.token_start, doc.commands, doc.states)
-    (new_doc, changes.toList)
+    (changes.toList, new_doc)
   }
 }
 
@@ -71,7 +69,7 @@
 {
   /* token view */
 
-  def text_edit(session: Session, e: Text_Edit): (Document_Body, List[Document.Structure_Edit]) =
+  def text_edit(session: Session, e: Text_Edit): (Document_Body, List[Document.Edit]) =
   {
     case class TextChange(start: Int, added: String, removed: String)
     val change = e match {
@@ -158,7 +156,7 @@
       inserted_tokens: List[Token],
       after_change: Option[Token],
       new_tokens: List[Token],
-      new_token_start: Map[Token, Int]): (Document_Body, Document.Structure_Change) =
+      new_token_start: Map[Token, Int]): (Document_Body, List[Document.Edit]) =
   {
     val new_tokenset = Linear_Set[Token]() ++ new_tokens
     val cmd_before_change = before_change match {
@@ -260,6 +258,7 @@
   /* command/state assignment */
 
   val assignment = Future.promise[Map[Command, Command]]
+  def await_assignment { assignment.join }
 
   @volatile private var tmp_states = old_states
 
diff -r d21c997104c4 -r 32b49207ca20 src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Sun Jan 10 15:42:31 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Sun Jan 10 16:40:21 2010 +0100
@@ -81,7 +81,7 @@
     {
       require(change.parent.isDefined)
 
-      val (doc, changes) = change.result.join
+      val (changes, doc) = change.result.join
       val id_changes = changes map {
         case (c1, c2) =>
           (c1.map(_.id).getOrElse(""),