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

--- 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]]