# HG changeset patch
# User wenzelm
# Date 1262191738 -3600
# Node ID f0107bc96961696c30cbc07ff7132793fb314fd3
# Parent  4c875ed8b248f121d9fbb14f307ada813a9ad9b2
more explicit modeling of Command and Command_State as Session.Entity;
misc tuning;

diff -r 4c875ed8b248 -r f0107bc96961 src/Tools/jEdit/src/proofdocument/command.scala
--- a/src/Tools/jEdit/src/proofdocument/command.scala	Wed Dec 30 13:21:46 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/command.scala	Wed Dec 30 17:48:58 2009 +0100
@@ -51,14 +51,17 @@
 
 
 class Command(
-    val id: String,
+    val id: Isar_Document.Command_ID,
     val tokens: List[Token],
-    val starts: Map[Token, Int]) extends Accumulator
+    val starts: Map[Token, Int]) extends Accumulator with Session.Entity
 {
   require(!tokens.isEmpty)
 
+  // FIXME override equality as well
   override def hashCode = id.hashCode
 
+  def consume(session: Session, message: XML.Tree) { this ! (session, message) }
+
 
   /* content */
 
@@ -91,8 +94,8 @@
 
   /* results, markup, ... */
 
-  private val empty_cmd_state = new Command_State(this)
-  private def cmd_state(doc: Proof_Document) =
+  private val empty_cmd_state = new Command_State("", this)  // FIXME ?
+  private def cmd_state(doc: Proof_Document) =  // FIXME clarify
     doc.states.getOrElse(this, empty_cmd_state)
 
   def status(doc: Proof_Document) = cmd_state(doc).state.status
@@ -104,10 +107,14 @@
 }
 
 
-class Command_State(val command: Command) extends Accumulator
+class Command_State(
+  override val id: Isar_Document.State_ID,
+  val command: Command) extends Accumulator with Session.Entity
 {
   protected override var _state = new State(command)
 
+  def consume(session: Session, message: XML.Tree) { this ! (session, message) }
+
   def results: List[XML.Tree] =
     command.state.results ::: state.results
 
diff -r 4c875ed8b248 -r f0107bc96961 src/Tools/jEdit/src/proofdocument/session.scala
--- a/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 13:21:46 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 17:48:58 2009 +0100
@@ -11,7 +11,20 @@
 
 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
+  }
 }
 
 
@@ -30,7 +43,7 @@
   /* 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 */
@@ -90,12 +103,12 @@
     {
       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) {
@@ -111,7 +124,7 @@
                   {
                     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!?
diff -r 4c875ed8b248 -r f0107bc96961 src/Tools/jEdit/src/proofdocument/state.scala
--- a/src/Tools/jEdit/src/proofdocument/state.scala	Wed Dec 30 13:21:46 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/state.scala	Wed Dec 30 17:48:58 2009 +0100
@@ -11,7 +11,7 @@
 class State(
   val command: Command,
   val status: Command.Status.Value,
-  rev_results: List[XML.Tree],
+  val rev_results: List[XML.Tree],
   val markup_root: Markup_Text)
 {
   def this(command: Command) =