maintain generic session entities -- cover commands, states, etc. (but not yet documents);

--- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Dec 30 19:58:22 2009 +0100
+++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Dec 30 20:18:50 2009 +0100
@@ -55,11 +55,11 @@
                   case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
                     new External_Hyperlink(begin, end, line, ref_file, ref_line)
                   case Command.RefInfo(_, _, Some(id), Some(offset)) =>
-                    Isabelle.session.command(id) match {
-                      case Some(ref_cmd) =>
+                    Isabelle.session.lookup_entity(id) match {
+                      case Some(ref_cmd: Command) =>
                         new Internal_Hyperlink(begin, end, line,
                           model.to_current(document, ref_cmd.start(document) + offset - 1))
-                      case None => null
+                      case _ => null
                     }
                   case _ => null
                 }

--- a/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 19:58:22 2009 +0100
+++ b/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 20:18:50 2009 +0100
@@ -52,17 +52,16 @@
   @volatile private var outer_syntax = new Outer_Syntax(system.symbols)
   def syntax(): Outer_Syntax = outer_syntax
 
-  @volatile private var states = Map[Isar_Document.State_ID, Command]()
-  @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
+  @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
+  def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
+
   @volatile private var documents = Map[Isar_Document.Document_ID, Proof_Document]()
-
-  def state(id: Isar_Document.State_ID): Option[Command] = states.get(id)
-  def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
   def document(id: Isar_Document.Document_ID): Option[Proof_Document] = documents.get(id)
 
 
   /** main actor **/
 
+  private case class Register(entity: Session.Entity)
   private case class Start(args: List[String])
   private case object Stop
   private case class Begin_Document(path: String)
@@ -72,6 +71,8 @@
     var prover: Isabelle_Process with Isar_Document = null
     var prover_ready = false
 
+    def register(entity: Session.Entity) { entities += (entity.id -> entity) }
+
 
     /* document changes */
 
@@ -86,7 +87,7 @@
            c2 match {
               case None => None
               case Some(command) =>  // FIXME clarify -- may reuse existing commands!??
-                commands += (command.id -> command)
+                register(command)
                 prover.define_command(command.id, system.symbols.encode(command.content))
                 Some(command.id)
             })
@@ -107,7 +108,7 @@
       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
+          case Some(id) => entities.get(id)
         }
       if (target.isDefined) target.get.consume(this, result.message)
       else if (result.kind == Isabelle_Process.Kind.STATUS) {
@@ -123,13 +124,13 @@
                     XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
                     <- edits }
                   {
-                    commands.get(cmd_id) match {
-                      case Some(cmd) =>
+                    entities.get(cmd_id) match {
+                      case Some(cmd: Command) =>
                         val state = cmd.finish_static(state_id)
-                        states += (state_id -> state)
-                        doc.states += (cmd -> state)
+                        register(state)
+                        doc.states += (cmd -> state)  // FIXME !?
                         command_change.event(cmd)   // FIXME really!?
-                      case None =>
+                      case _ =>
                     }
                   }
               }
@@ -159,6 +160,10 @@
 
     loop {
       react {
+        case Register(entity: Session.Entity) =>
+          register(entity)
+          reply(())
+
         case Start(args) =>
           if (prover == null) {
             prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
@@ -192,6 +197,8 @@
 
   /* main methods */
 
+  def register_entity(entity: Session.Entity) { session_actor !? Register(entity) }
+
   def start(args: List[String]) { session_actor !? Start(args) }
   def stop() { session_actor ! Stop }
   def input(change: Change) { session_actor ! change }