src/Tools/jEdit/src/proofdocument/session.scala

--- a/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 20:26:08 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 21:34:33 2009 +0100
@@ -55,10 +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)
 
+  // FIXME eliminate
   @volatile private var documents = Map[Isar_Document.Document_ID, Proof_Document]()
   def document(id: Isar_Document.Document_ID): Option[Proof_Document] = documents.get(id)
 
 
+
   /** main actor **/
 
   private case class Register(entity: Session.Entity)
@@ -92,6 +94,7 @@
                 Some(command.id)
             })
       }
+      register(doc)
       documents += (doc.id -> doc)
       prover.edit_document(old.id, doc.id, id_changes)
 
@@ -112,29 +115,9 @@
         }
       if (target.isDefined) target.get.consume(this, result.message)
       else if (result.kind == Isabelle_Process.Kind.STATUS) {
-        //{{{ global status message
+        // global status message
         for (elem <- result.body) {
           elem match {
-            // document edits
-            case XML.Elem(Markup.EDITS, (Markup.ID, doc_id) :: _, edits) =>
-              document(doc_id) match {
-                case None =>  // FIXME clarify
-                case Some(doc) =>
-                  for {
-                    XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
-                    <- edits }
-                  {
-                    entities.get(cmd_id) match {
-                      case Some(cmd: Command) =>
-                        val state = cmd.finish_static(state_id)
-                        register(state)
-                        doc.states += (cmd -> state)  // FIXME !?
-                        command_change.event(cmd)   // FIXME really!?
-                      case _ =>
-                    }
-                  }
-              }
-
             // command and keyword declarations
             case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
               outer_syntax += (name, kind)
@@ -147,7 +130,6 @@
           case _ =>
           }
         }
-        //}}}
       }
       else if (result.kind == Isabelle_Process.Kind.EXIT)
         prover = null
@@ -178,6 +160,7 @@
         case Begin_Document(path: String) if prover_ready =>
           val id = create_id()
           val doc = Proof_Document.empty(id)
+          register(doc)
           documents += (id -> doc)
           prover.begin_document(id, path)
           reply(doc)