added EventBus for new command- or keyword-declarations
authorimmler@in.tum.de
Sun, 11 Jan 2009 13:16:35 +0100
changeset 34465 ccadbf63e320
parent 34464 8a1ba195247a
child 34466 191a481f0594
added EventBus for new command- or keyword-declarations
src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Sun Jan 11 13:15:05 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Sun Jan 11 13:16:35 2009 +0100
@@ -24,8 +24,19 @@
   private var process: Isar = null
   private var commands = new HashMap[String, Command]
 
-  val command_decls = new HashSet[String]
-  val keyword_decls = new HashSet[String]
+  val decl_info = new EventBus[(String, String)]
+  val command_decls = new HashSet[String]{
+    override def +=(elem : String) = {
+      decl_info.event(elem, Markup.COMMAND)
+      this += elem
+    }
+  }
+  val keyword_decls = new HashSet[String]{
+    override def +=(elem : String) = {
+      decl_info.event(elem, Markup.KEYWORD)
+      this += elem
+    }
+  }
   private var initialized = false
 
   val activated = new EventBus[Unit]