1.1 --- a/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Mon Sep 07 21:09:26 2009 +0200
     1.2 +++ b/src/Tools/jEdit/src/jedit/IsabelleSideKickParser.scala	Mon Sep 07 22:17:51 2009 +0200
     1.3 @@ -86,7 +86,7 @@
     1.4      val text = buffer.getSegment(start, caret - start)
     1.5  
     1.6      val completion =
     1.7 -      Isabelle.prover_setup(buffer).map(_.prover.completion).getOrElse(Isabelle.completion)
     1.8 +      Isabelle.prover_setup(buffer).map(_.prover.completion()).getOrElse(Isabelle.completion)
     1.9  
    1.10      completion.complete(text) match {
    1.11        case None => null

     2.1 --- a/src/Tools/jEdit/src/jedit/Plugin.scala	Mon Sep 07 21:09:26 2009 +0200
     2.2 +++ b/src/Tools/jEdit/src/jedit/Plugin.scala	Mon Sep 07 22:17:51 2009 +0200
     2.3 @@ -87,7 +87,7 @@
     2.4    /* Isabelle font */
     2.5  
     2.6    var font: Font = null
     2.7 -  val font_changed = new EventBus[Font]
     2.8 +  val font_changed = new Event_Bus[Font]
     2.9  
    2.10    def set_font(size: Int)
    2.11    {
    2.12 @@ -100,9 +100,9 @@
    2.13  
    2.14    /* event buses */
    2.15  
    2.16 -  val state_update = new EventBus[Command]
    2.17 -  val command_change = new EventBus[Command]
    2.18 -  val document_change = new EventBus[ProofDocument]
    2.19 +  val state_update = new Event_Bus[Command]
    2.20 +  val command_change = new Event_Bus[Command]
    2.21 +  val document_change = new Event_Bus[ProofDocument]
    2.22  
    2.23  
    2.24    /* selected state */

     3.1 --- a/src/Tools/jEdit/src/prover/Prover.scala	Mon Sep 07 21:09:26 2009 +0200
     3.2 +++ b/src/Tools/jEdit/src/prover/Prover.scala	Mon Sep 07 22:17:51 2009 +0200
     3.3 @@ -37,6 +37,18 @@
     3.4    def stop() { process.kill }
     3.5  
     3.6    
     3.7 +  /* outer syntax keywords and completion */
     3.8 +
     3.9 +  @volatile private var _keyword_decls = Set[String]()
    3.10 +  def keyword_decls() = _keyword_decls
    3.11 +
    3.12 +  @volatile private var _command_decls = Map[String, String]()
    3.13 +  def command_decls() = _command_decls
    3.14 +
    3.15 +  @volatile private var _completion = Isabelle.completion
    3.16 +  def completion() = _completion
    3.17 +
    3.18 +
    3.19    /* document state information */
    3.20  
    3.21    private val states = new mutable.HashMap[Isar_Document.State_ID, Command_State] with
    3.22 @@ -45,46 +57,17 @@
    3.23      mutable.SynchronizedMap[Isar_Document.Command_ID, Command]
    3.24    val document_0 =
    3.25      ProofDocument.empty.
    3.26 -      set_command_keyword(command_decls.contains).
    3.27 +      set_command_keyword((s: String) => command_decls().contains(s)).
    3.28        set_change_receiver(change_receiver)
    3.29    private var document_versions = List(document_0)
    3.30  
    3.31    def command(id: Isar_Document.Command_ID): Option[Command] = commands.get(id)
    3.32    def document(id: Isar_Document.Document_ID) = document_versions.find(_.id == id)
    3.33 -
    3.34    
    3.35 -  /* outer syntax keywords */
    3.36 -
    3.37 -  val decl_info = new EventBus[(String, String)]
    3.38 -
    3.39 -  private val keyword_decls =
    3.40 -    new mutable.HashSet[String] with mutable.SynchronizedSet[String] {
    3.41 -    override def +=(name: String) = {
    3.42 -      decl_info.event(name, OuterKeyword.MINOR)
    3.43 -      super.+=(name)
    3.44 -    }
    3.45 -  }
    3.46 -  private val command_decls =
    3.47 -    new mutable.HashMap[String, String] with mutable.SynchronizedMap[String, String] {
    3.48 -    override def +=(entry: (String, String)) = {
    3.49 -      decl_info.event(entry)
    3.50 -      super.+=(entry)
    3.51 -    }
    3.52 -  }
    3.53 -
    3.54 -
    3.55 -  /* completions */
    3.56 -
    3.57 -  private var _completion = Isabelle.completion
    3.58 -  def completion = _completion
    3.59 -  decl_info += (p => _completion += p._1)
    3.60 -
    3.61  
    3.62    /* event handling */
    3.63 -  lazy val output_info = new EventBus[Isabelle_Process.Result]
    3.64  
    3.65    val output_text_view = new JTextArea
    3.66 -  output_info += (result => output_text_view.append(result.toString + "\n"))
    3.67  
    3.68    private case object Ready
    3.69  
    3.70 @@ -98,7 +81,8 @@
    3.71            else if (states.contains(id)) Some(states(id))
    3.72            else None
    3.73        }
    3.74 -    output_info.event(result)
    3.75 +    Swing_Thread.later { output_text_view.append(result.toString + "\n") }  // slow?
    3.76 +
    3.77      val message = Isabelle_Process.parse_message(isabelle_system, result)
    3.78  
    3.79      if (state.isDefined) state.get ! message
    3.80 @@ -114,9 +98,11 @@
    3.81                  // command and keyword declarations
    3.82                  case XML.Elem(Markup.COMMAND_DECL,
    3.83                      (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
    3.84 -                  command_decls += (name -> kind)
    3.85 +                  _command_decls += (name -> kind)
    3.86 +                  _completion += name
    3.87                  case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
    3.88 -                  keyword_decls += name
    3.89 +                  _keyword_decls += name
    3.90 +                  _completion += name
    3.91  
    3.92                  // process ready (after initialization)
    3.93                  case XML.Elem(Markup.READY, _, _) => this ! Ready