# HG changeset patch
# User wenzelm
# Date 1231706938 -3600
# Node ID 1dac4749286354c53b8d937e92d975db18e8006c
# Parent  f4c033b3363092a538eb897cf8129c5b844fabb1
decl_info: cover both commands and keywords, with kind;
command_decls: maintain kinds as well (Map);

diff -r f4c033b33630 -r 1dac47492863 src/Tools/jEdit/src/prover/Prover.scala
--- a/src/Tools/jEdit/src/prover/Prover.scala	Sun Jan 11 21:48:12 2009 +0100
+++ b/src/Tools/jEdit/src/prover/Prover.scala	Sun Jan 11 21:48:58 2009 +0100
@@ -25,16 +25,16 @@
   private var commands = new HashMap[String, Command]
 
   val decl_info = new EventBus[(String, String)]
-  val command_decls = new HashSet[String]{
-    override def +=(elem : String) = {
-      decl_info.event(elem, Markup.COMMAND)
-      super.+=(elem)
+  val command_decls = new HashMap[String, String] {
+    override def +=(entry: (String, String)) = {
+      decl_info.event(entry)
+      super.+=(entry)
     }
   }
-  val keyword_decls = new HashSet[String]{
-    override def +=(elem : String) = {
-      decl_info.event(elem, Markup.KEYWORD)
-      super.+=(elem)
+  val keyword_decls = new HashSet[String] {
+    override def +=(name: String) = {
+      decl_info.event(name, OuterKeyword.MINOR)
+      super.+=(name)
     }
   }
   private var initialized = false
@@ -90,8 +90,9 @@
                       command_change(st)
 
                     // command and keyword declarations
-                    case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: _, _) =>
-                      command_decls += name
+                    case XML.Elem(Markup.COMMAND_DECL,
+                        (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
+                      command_decls += (name -> kind)
                     case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
                       keyword_decls += name