back to explicit management of documents -- not as generic Session.Entity -- to avoid ill-defined referencing of new states;
recent_document: require finished state assignment;
explicitly typed Session.lookup_command;

--- a/src/Tools/jEdit/src/jedit/document_model.scala	Mon Jan 04 00:13:09 2010 +0100
+++ b/src/Tools/jEdit/src/jedit/document_model.scala	Mon Jan 04 19:08:10 2010 +0100
@@ -68,7 +68,8 @@
   def recent_document(): Document =
   {
     def find(change: Change): Document =
-      if (change.result.is_finished || !change.parent.isDefined) change.document
+      if (change.result.is_finished && change.document.is_assigned || !change.parent.isDefined)
+        change.document
       else find(change.parent.get)
     find(current_change())
   }

--- a/src/Tools/jEdit/src/proofdocument/command.scala	Mon Jan 04 00:13:09 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/command.scala	Mon Jan 04 19:08:10 2010 +0100
@@ -73,7 +73,7 @@
           state = state.+(session, message)
 
         case Assign =>
-          assigned = true  // single assigment
+          assigned = true  // single assignment
           reply(())
 
         case bad => System.err.println("command accumulator: ignoring bad message " + bad)

--- a/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 04 00:13:09 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/document.scala	Mon Jan 04 19:08:10 2010 +0100
@@ -34,7 +34,11 @@
       "[()\\[\\]{}:;]", Pattern.MULTILINE)
 
   def empty(id: Isar_Document.Document_ID): Document =
-    new Document(id, Linear_Set(), Map(), Linear_Set(), Map())
+  {
+    val doc = new Document(id, Linear_Set(), Map(), Linear_Set(), Map())
+    doc.assign_states(Nil)
+    doc
+  }
 
   type Structure_Edit = (Option[Command], Option[Command])
   type Structure_Change = List[Structure_Edit]
@@ -61,46 +65,29 @@
     val token_start: Map[Token, Int],  // FIXME eliminate
     val commands: Linear_Set[Command],
     old_states: Map[Command, Command])
-  extends Session.Entity
 {
   def content = Token.string_from_tokens(Nil ++ tokens, token_start)
 
 
-  /* accumulated messages */
+  /* command/state assignment */
+
+  val assignment = Future.promise[Map[Command, Command]]
+  def is_assigned = assignment.is_finished
 
-  @volatile private var states = old_states
+  @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 =
-    states.getOrElse(cmd, cmd).current_state
-
-  private val accumulator = actor {
-    loop {
-      react {
-        case (session: Session, message: XML.Tree) =>
-          message match {
-            case XML.Elem(Markup.MESSAGE, (Markup.CLASS, Markup.STATUS) :: _, elems) =>
-              for {
-                XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
-                  <- elems
-              } {
-                session.lookup_entity(cmd_id) match {
-                  case Some(cmd: Command) =>
-                    val state = cmd.assign_state(state_id)
-                    session.register_entity(state)
-                    states += (cmd -> state)
-                  case _ =>
-                }
-              }
-            case _ =>
-          }
-
-        case bad => System.err.println("document accumulator: ignoring bad message " + bad)
-      }
-    }
+  {
+    require(assignment.is_finished)
+    (assignment.join)(cmd).current_state
   }
 
-  def consume(session: Session, message: XML.Tree) { accumulator ! (session, message) }
-
 
 
   /** token view **/
@@ -196,6 +183,8 @@
       new_token_start: Map[Token, Int]):
     Document.Result =
   {
+    require(assignment.is_finished)
+
     val new_tokenset = Linear_Set[Token]() ++ new_tokens
     val cmd_before_change = before_change match {
       case None => None
@@ -273,7 +262,7 @@
 
     val doc =
       new Document(new_id, new_tokenset, new_token_start, new_commandset,
-        states -- removed_commands)
+        assignment.join -- removed_commands)
 
     val removes =
       for (cmd <- removed_commands) yield (cmd_before_change -> None)

--- a/src/Tools/jEdit/src/proofdocument/session.scala	Mon Jan 04 00:13:09 2010 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Mon Jan 04 19:08:10 2010 +0100
@@ -55,8 +55,12 @@
 
   @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
   def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
+  def lookup_command(id: Session.Entity_ID): Option[Command] =
+    lookup_entity(id) match {
+      case Some(cmd: Command) => Some(cmd)
+      case _ => None
+    }
 
-  private case class Register(entity: Session.Entity)
   private case class Start(timeout: Int, args: List[String])
   private case object Stop
   private case class Begin_Document(path: String)
@@ -67,6 +71,9 @@
 
     def register(entity: Session.Entity) { entities += (entity.id -> entity) }
 
+    var documents = Map[Isar_Document.Document_ID, Document]()
+    def register_document(doc: Document) { documents += (doc.id -> doc) }
+
 
     /* document changes */
 
@@ -80,13 +87,15 @@
           (c1.map(_.id).getOrElse(""),
            c2 match {
               case None => None
-              case Some(command) =>  // FIXME register/define only commands unknown to prover
-                register(command)
-                prover.define_command(command.id, system.symbols.encode(command.content))
+              case Some(command) =>
+                if (!lookup_command(command.id).isDefined) {
+                  register(command)
+                  prover.define_command(command.id, system.symbols.encode(command.content))
+                }
                 Some(command.id)
             })
       }
-      register(doc)
+      register_document(doc)
       prover.edit_document(change.parent.get.id, doc.id, id_changes)
     }
 
@@ -97,16 +106,35 @@
     {
       raw_results.event(result)
 
+      val target_id: Option[Session.Entity_ID] = Position.get_id(result.props)
       val target: Option[Session.Entity] =
-        Position.get_id(result.props) match {
+        target_id match {
           case None => None
-          case Some(id) => entities.get(id)
+          case Some(id) => lookup_entity(id)
         }
       if (target.isDefined) target.get.consume(this, result.message)
       else if (result.kind == Isabelle_Process.Kind.STATUS) {
         // global status message
         for (elem <- result.body) {
           elem match {
+            // document state assigment
+            case XML.Elem(Markup.ASSIGN, _, edits) if target_id.isDefined =>
+              documents.get(target_id.get) match {
+                case Some(doc) =>
+                  val states =
+                    for {
+                      XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
+                        <- edits
+                      cmd <- lookup_command(cmd_id)
+                    } yield {
+                      val st = cmd.assign_state(state_id)
+                      register(st)
+                      (cmd, st)
+                    }
+                  doc.assign_states(states)
+                case None =>
+              }
+
             // command and keyword declarations
             case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
               syntax += (name, kind)
@@ -167,10 +195,6 @@
 
     loop {
       react {
-        case Register(entity: Session.Entity) =>
-          register(entity)
-          reply(())
-
         case Start(timeout, args) =>
           if (prover == null) {
             prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
@@ -190,7 +214,7 @@
         case Begin_Document(path: String) if prover != null =>
           val id = create_id()
           val doc = Document.empty(id)
-          register(doc)
+          register_document(doc)
           prover.begin_document(id, path)
           reply(doc)
 
@@ -209,8 +233,6 @@
 
   /* main methods */
 
-  def register_entity(entity: Session.Entity) { session_actor !? Register(entity) }
-
   def start(timeout: Int, args: List[String]): Option[String] =
     (session_actor !? Start(timeout, args)).asInstanceOf[Option[String]]