# HG changeset patch
# User wenzelm
# Date 1262205273 -3600
# Node ID 7df68a8f0e3e89f399e334200825f709e747495d
# Parent  b4efd0ef2f3eeb5c29c73514dbd4d90e28316fe7
register Proof_Document instances as session entities -- handle Markup.EDIT messages locally;

diff -r b4efd0ef2f3e -r 7df68a8f0e3e src/Tools/jEdit/src/proofdocument/proof_document.scala
--- a/src/Tools/jEdit/src/proofdocument/proof_document.scala	Wed Dec 30 20:26:08 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/proof_document.scala	Wed Dec 30 21:34:33 2009 +0100
@@ -9,22 +9,24 @@
 package isabelle.proofdocument
 
 
+import scala.actors.Actor._
+
 import java.util.regex.Pattern
 
 
 object Proof_Document
 {
   // Be careful when changing this regex. Not only must it handle the
-  // spurious end of a token but also:  
+  // spurious end of a token but also:
   // Bug ID: 5050507 Pattern.matches throws StackOverflow Error
   // http://bugs.sun.com/bugdatabase/view_bug.do?bug_id=5050507
-  
-  val token_pattern = 
+
+  val token_pattern =
     Pattern.compile(
       "\\{\\*([^*]|\\*[^}]|\\*\\z)*(\\z|\\*\\})|" +
       "\\(\\*([^*]|\\*[^)]|\\*\\z)*(\\z|\\*\\))|" +
-      "(\\?'?|')[A-Za-z_0-9.]*|" + 
-      "[A-Za-z_0-9.]+|" + 
+      "(\\?'?|')[A-Za-z_0-9.]*|" +
+      "[A-Za-z_0-9.]+|" +
       "[!#$%&*+-/<=>?@^_|~]+|" +
       "\"([^\\\\\"]?(\\\\(.|\\z))?)*+(\"|\\z)|" +
       "`([^\\\\`]?(\\\\(.|\\z))?)*+(`|\\z)|" +
@@ -38,18 +40,51 @@
 
 
 class Proof_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],
-  var states: Map[Command, Command])   // FIXME immutable, eliminate!?
+    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],
+    var states: Map[Command, Command])   // FIXME immutable, eliminate!?
+  extends Session.Entity
 {
   import Proof_Document.StructureChange
 
   def content = Token.string_from_tokens(Nil ++ tokens, token_start)
 
 
-  
+  /* accumulated messages */
+
+  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.finish_static(state_id)
+                    session.register_entity(state)
+                    states += (cmd -> state)  // FIXME !?
+                    session.command_change.event(cmd)   // FIXME really!?
+                  case _ =>
+                }
+              }
+            case _ =>
+          }
+
+        case bad => System.err.println("document accumulator: ignoring bad message " + bad)
+      }
+    }
+  }
+
+  def consume(session: Session, message: XML.Tree) { accumulator ! (session, message) }
+
+
+
   /** token view **/
 
   def text_changed(session: Session, change: Change): (Proof_Document, StructureChange) =
@@ -101,7 +136,7 @@
 
     val ins = new Token(change.added, Token.Kind.OTHER)
     start += (ins -> change.start)
-    
+
     var invalid_tokens = split_begin ::: ins :: split_end ::: end
     var new_tokens: List[Token] = Nil
     var old_suffix: List[Token] = Nil
@@ -140,7 +175,7 @@
       old_suffix.firstOption, new_token_list, start)
   }
 
-  
+
   /** command view **/
 
   private def token_changed(
diff -r b4efd0ef2f3e -r 7df68a8f0e3e 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)