# HG changeset patch
# User wenzelm
# Date 1262817960 -3600
# Node ID 6c5560d48561a5f15b2614fa4f97ca8be35f057b
# Parent  3457436a1110f89a54cf0d6efa044b9b090d58ab
more precise treatment of document/state assigment;

diff -r 3457436a1110 -r 6c5560d48561 src/Tools/jEdit/src/jedit/document_model.scala
--- a/src/Tools/jEdit/src/jedit/document_model.scala	Tue Jan 05 18:29:21 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Wed Jan 06 23:46:00 2010 +0100
@@ -67,11 +67,10 @@
 
   def recent_document(): Document =
   {
-    def find(change: Change): Document =
-      if (change.result.is_finished && change.document.is_assigned || !change.parent.isDefined)
-        change.document
+    def find(change: Change): Change =
+      if (change.result.is_finished && change.document.assignment.is_finished) change
       else find(change.parent.get)
-    find(current_change())
+    find(current_change()).document
   }
 
 
diff -r 3457436a1110 -r 6c5560d48561 src/Tools/jEdit/src/proofdocument/document.scala
--- a/src/Tools/jEdit/src/proofdocument/document.scala	Tue Jan 05 18:29:21 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/document.scala	Wed Jan 06 23:46:00 2010 +0100
@@ -47,52 +47,31 @@
   def text_edits(session: Session, old_doc: Document, new_id: Isar_Document.Document_ID,
     edits: List[Text_Edit]): Result =
   {
+    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 new_doc = (old_doc /: edits)((doc1: Document, edit: Text_Edit) =>
+    val doc = (doc0 /: edits)((doc1: Document_Body, edit: Text_Edit) =>
       {
-        val (doc2, chgs) = doc1.text_edit(session, edit, new_id)  // FIXME odd multiple use of id
+        val (doc2, chgs) = doc1.text_edit(session, edit)
         changes ++ chgs
         doc2
       })
+    val new_doc = new Document(new_id, doc.tokens, doc.token_start, doc.commands, doc.states)
     (new_doc, changes.toList)
   }
 }
 
-
-class Document(
-    val id: Isar_Document.Document_ID,
-    val tokens: Linear_Set[Token],   // FIXME plain List, inside Command
-    val token_start: Map[Token, Int],  // FIXME eliminate
-    val commands: Linear_Set[Command],
-    old_states: Map[Command, Command])
+private case class Document_Body(
+  val tokens: Linear_Set[Token],   // FIXME plain List, inside Command
+  val token_start: Map[Token, Int],  // FIXME eliminate
+  val commands: Linear_Set[Command],
+  val states: Map[Command, Command])
 {
-  def content = Token.string_from_tokens(Nil ++ tokens, token_start)
-
-
-  /* command/state assignment */
-
-  val assignment = Future.promise[Map[Command, Command]]
-  def is_assigned = assignment.is_finished
-
-  @volatile private var tmp_states = old_states
+  /* token view */
 
-  def assign_states(new_states: List[(Command, Command)])
-  {
-    assignment.fulfill(tmp_states ++ new_states)
-    tmp_states = Map()
-  }
-
-  def current_state(cmd: Command): State =
-  {
-    require(assignment.is_finished)
-    (assignment.join)(cmd).current_state
-  }
-
-
-
-  /** token view **/
-
-  def text_edit(session: Session, e: Text_Edit, id: String): Document.Result =
+  def text_edit(session: Session, e: Text_Edit): (Document_Body, List[Document.Structure_Edit]) =
   {
     case class TextChange(start: Int, added: String, removed: String)
     val change = e match {
@@ -166,25 +145,21 @@
     }
     val insert = new_tokens.reverse
     val new_token_list = begin ::: insert ::: old_suffix
-    token_changed(session, id, begin.lastOption, insert,
+    token_changed(session, begin.lastOption, insert,
       old_suffix.firstOption, new_token_list, start)
   }
 
 
-  /** command view **/
+  /* command view */
 
   private def token_changed(
       session: Session,
-      new_id: String,
       before_change: Option[Token],
       inserted_tokens: List[Token],
       after_change: Option[Token],
       new_tokens: List[Token],
-      new_token_start: Map[Token, Int]):
-    Document.Result =
+      new_token_start: Map[Token, Int]): (Document_Body, Document.Structure_Change) =
   {
-    require(assignment.is_finished)
-
     val new_tokenset = Linear_Set[Token]() ++ new_tokens
     val cmd_before_change = before_change match {
       case None => None
@@ -261,16 +236,45 @@
 
 
     val doc =
-      new Document(new_id, new_tokenset, new_token_start, new_commandset,
-        assignment.join -- removed_commands)
+      new Document_Body(new_tokenset, new_token_start, new_commandset, states -- removed_commands)
 
     val removes =
       for (cmd <- removed_commands) yield (cmd_before_change -> None)
     val inserts =
       for (cmd <- inserted_commands) yield (doc.commands.prev(cmd) -> Some(cmd))
 
-    return (doc, removes.toList ++ inserts)
+    (doc, removes.toList ++ inserts)
   }
+}
+
+class Document(
+    val id: Isar_Document.Document_ID,
+    val tokens: Linear_Set[Token],   // FIXME plain List, inside Command
+    val token_start: Map[Token, Int],  // FIXME eliminate
+    val commands: Linear_Set[Command],
+    old_states: Map[Command, Command])
+{
+  def content = Token.string_from_tokens(Nil ++ tokens, token_start)
+
+
+  /* command/state assignment */
+
+  val assignment = Future.promise[Map[Command, Command]]
+
+  @volatile private var tmp_states = old_states
+
+  def assign_states(new_states: List[(Command, Command)])
+  {
+    assignment.fulfill(tmp_states ++ new_states)
+    tmp_states = Map()
+  }
+
+  def current_state(cmd: Command): State =
+  {
+    require(assignment.is_finished)
+    (assignment.join)(cmd).current_state
+  }
+
 
   val commands_offsets = {
     var last_stop = 0