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

 
 import scala.actors.Actor._
 
 object Session
 {
+  /* events */
+
   case object Global_Settings
+
+
+  /* managed entities */
+
+  type Entity_ID = String
+
+  trait Entity
+  {
+    val id: Entity_ID
+    def consume(session: Session, message: XML.Tree): Unit
+  }
 }
 
 
 class Session(system: Isabelle_System)
 {

 
 
   /* unique ids */
 
   private var id_count: BigInt = 0
-  def create_id(): String = synchronized { id_count += 1; "j" + id_count }
+  def create_id(): Session.Entity_ID = synchronized { id_count += 1; "j" + id_count }
 
 
   /* document state information -- owned by session_actor */
 
   @volatile private var outer_syntax = new Outer_Syntax(system.symbols)

 
     def handle_result(result: Isabelle_Process.Result)
     {
       raw_results.event(result)
 
-      val state =
+      val target: Option[Session.Entity] =
         Position.id_of(result.props) match {
           case None => None
           case Some(id) => commands.get(id) orElse states.get(id) orElse None
         }
-      if (state.isDefined) state.get ! (this, result.message)
+      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 edits

                     XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
                     <- edits }
                   {
                     commands.get(cmd_id) match {
                       case Some(cmd) =>
-                        val state = new Command_State(cmd)
+                        val state = new Command_State(state_id, cmd)
                         states += (state_id -> state)
                         doc.states += (cmd -> state)
                         command_change.event(cmd)   // FIXME really!?
                       case None =>
                     }