1.1 --- a/src/Pure/Isar/outer_syntax.scala	Thu Mar 15 09:55:42 2012 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Thu Mar 15 10:16:21 2012 +0100
     1.3 @@ -34,6 +34,7 @@
     1.4      result.toString
     1.5    }
     1.6  
     1.7 +  type Decl = (String, Option[(String, List[String])])
     1.8    def init(): Outer_Syntax = new Outer_Syntax()
     1.9  }
    1.10  
    1.11 @@ -51,8 +52,12 @@
    1.12        if (Keyword.control(kind)) completion else completion + (name, replace))
    1.13  
    1.14    def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
    1.15 -
    1.16    def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
    1.17 +  def + (decl: Outer_Syntax.Decl): Outer_Syntax =
    1.18 +    decl match {
    1.19 +      case ((name, Some((kind, _)))) => this + (name, kind)
    1.20 +      case ((name, None)) => this + name
    1.21 +    }
    1.22  
    1.23    def is_command(name: String): Boolean =
    1.24      keyword_kind(name) match {