1.1 --- a/src/Tools/jEdit/src/prover/Prover.scala	Sun Jan 11 21:48:12 2009 +0100
     1.2 +++ b/src/Tools/jEdit/src/prover/Prover.scala	Sun Jan 11 21:48:58 2009 +0100
     1.3 @@ -25,16 +25,16 @@
     1.4    private var commands = new HashMap[String, Command]
     1.5  
     1.6    val decl_info = new EventBus[(String, String)]
     1.7 -  val command_decls = new HashSet[String]{
     1.8 -    override def +=(elem : String) = {
     1.9 -      decl_info.event(elem, Markup.COMMAND)
    1.10 -      super.+=(elem)
    1.11 +  val command_decls = new HashMap[String, String] {
    1.12 +    override def +=(entry: (String, String)) = {
    1.13 +      decl_info.event(entry)
    1.14 +      super.+=(entry)
    1.15      }
    1.16    }
    1.17 -  val keyword_decls = new HashSet[String]{
    1.18 -    override def +=(elem : String) = {
    1.19 -      decl_info.event(elem, Markup.KEYWORD)
    1.20 -      super.+=(elem)
    1.21 +  val keyword_decls = new HashSet[String] {
    1.22 +    override def +=(name: String) = {
    1.23 +      decl_info.event(name, OuterKeyword.MINOR)
    1.24 +      super.+=(name)
    1.25      }
    1.26    }
    1.27    private var initialized = false
    1.28 @@ -90,8 +90,9 @@
    1.29                        command_change(st)
    1.30  
    1.31                      // command and keyword declarations
    1.32 -                    case XML.Elem(Markup.COMMAND_DECL, (Markup.NAME, name) :: _, _) =>
    1.33 -                      command_decls += name
    1.34 +                    case XML.Elem(Markup.COMMAND_DECL,
    1.35 +                        (Markup.NAME, name) :: (Markup.KIND, kind) :: _, _) =>
    1.36 +                      command_decls += (name -> kind)
    1.37                      case XML.Elem(Markup.KEYWORD_DECL, (Markup.NAME, name) :: _, _) =>
    1.38                        keyword_decls += name
    1.39