1.1 --- a/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Dec 30 19:58:22 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/jedit/isabelle_hyperlinks.scala	Wed Dec 30 20:18:50 2009 +0100
     1.3 @@ -55,11 +55,11 @@
     1.4                    case Command.RefInfo(Some(ref_file), Some(ref_line), _, _) =>
     1.5                      new External_Hyperlink(begin, end, line, ref_file, ref_line)
     1.6                    case Command.RefInfo(_, _, Some(id), Some(offset)) =>
     1.7 -                    Isabelle.session.command(id) match {
     1.8 -                      case Some(ref_cmd) =>
     1.9 +                    Isabelle.session.lookup_entity(id) match {
    1.10 +                      case Some(ref_cmd: Command) =>
    1.11                          new Internal_Hyperlink(begin, end, line,
    1.12                            model.to_current(document, ref_cmd.start(document) + offset - 1))
    1.13 -                      case None => null
    1.14 +                      case _ => null
    1.15                      }
    1.16                    case _ => null
    1.17                  }

     2.1 --- a/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 19:58:22 2009 +0100
     2.2 +++ b/src/Tools/jEdit/src/proofdocument/session.scala	Wed Dec 30 20:18:50 2009 +0100
     2.3 @@ -52,17 +52,16 @@
     2.4    @volatile private var outer_syntax = new Outer_Syntax(system.symbols)
     2.5    def syntax(): Outer_Syntax = outer_syntax
     2.6  
     2.7 -  @volatile private var states = Map[Isar_Document.State_ID, Command]()
     2.8 -  @volatile private var commands = Map[Isar_Document.Command_ID, Command]()
     2.9 +  @volatile private var entities = Map[Session.Entity_ID, Session.Entity]()
    2.10 +  def lookup_entity(id: Session.Entity_ID): Option[Session.Entity] = entities.get(id)
    2.11 +
    2.12    @volatile private var documents = Map[Isar_Document.Document_ID, Proof_Document]()
    2.13 -
    2.14 -  def state(id: Isar_Document.State_ID): Option[Command] = states.get(id)
    2.15 -  def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
    2.16    def document(id: Isar_Document.Document_ID): Option[Proof_Document] = documents.get(id)
    2.17  
    2.18  
    2.19    /** main actor **/
    2.20  
    2.21 +  private case class Register(entity: Session.Entity)
    2.22    private case class Start(args: List[String])
    2.23    private case object Stop
    2.24    private case class Begin_Document(path: String)
    2.25 @@ -72,6 +71,8 @@
    2.26      var prover: Isabelle_Process with Isar_Document = null
    2.27      var prover_ready = false
    2.28  
    2.29 +    def register(entity: Session.Entity) { entities += (entity.id -> entity) }
    2.30 +
    2.31  
    2.32      /* document changes */
    2.33  
    2.34 @@ -86,7 +87,7 @@
    2.35             c2 match {
    2.36                case None => None
    2.37                case Some(command) =>  // FIXME clarify -- may reuse existing commands!??
    2.38 -                commands += (command.id -> command)
    2.39 +                register(command)
    2.40                  prover.define_command(command.id, system.symbols.encode(command.content))
    2.41                  Some(command.id)
    2.42              })
    2.43 @@ -107,7 +108,7 @@
    2.44        val target: Option[Session.Entity] =
    2.45          Position.id_of(result.props) match {
    2.46            case None => None
    2.47 -          case Some(id) => commands.get(id) orElse states.get(id) orElse None
    2.48 +          case Some(id) => entities.get(id)
    2.49          }
    2.50        if (target.isDefined) target.get.consume(this, result.message)
    2.51        else if (result.kind == Isabelle_Process.Kind.STATUS) {
    2.52 @@ -123,13 +124,13 @@
    2.53                      XML.Elem(Markup.EDIT, (Markup.ID, cmd_id) :: (Markup.STATE, state_id) :: _, _)
    2.54                      <- edits }
    2.55                    {
    2.56 -                    commands.get(cmd_id) match {
    2.57 -                      case Some(cmd) =>
    2.58 +                    entities.get(cmd_id) match {
    2.59 +                      case Some(cmd: Command) =>
    2.60                          val state = cmd.finish_static(state_id)
    2.61 -                        states += (state_id -> state)
    2.62 -                        doc.states += (cmd -> state)
    2.63 +                        register(state)
    2.64 +                        doc.states += (cmd -> state)  // FIXME !?
    2.65                          command_change.event(cmd)   // FIXME really!?
    2.66 -                      case None =>
    2.67 +                      case _ =>
    2.68                      }
    2.69                    }
    2.70                }
    2.71 @@ -159,6 +160,10 @@
    2.72  
    2.73      loop {
    2.74        react {
    2.75 +        case Register(entity: Session.Entity) =>
    2.76 +          register(entity)
    2.77 +          reply(())
    2.78 +
    2.79          case Start(args) =>
    2.80            if (prover == null) {
    2.81              prover = new Isabelle_Process(system, self, args:_*) with Isar_Document
    2.82 @@ -192,6 +197,8 @@
    2.83  
    2.84    /* main methods */
    2.85  
    2.86 +  def register_entity(entity: Session.Entity) { session_actor !? Register(entity) }
    2.87 +
    2.88    def start(args: List[String]) { session_actor !? Start(args) }
    2.89    def stop() { session_actor ! Stop }
    2.90    def input(change: Change) { session_actor ! change }