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 {

     2.1 --- a/src/Pure/PIDE/document.scala	Thu Mar 15 09:55:42 2012 +0100
     2.2 +++ b/src/Pure/PIDE/document.scala	Thu Mar 15 10:16:21 2012 +0100
     2.3 @@ -41,7 +41,7 @@
     2.4    {
     2.5      sealed case class Deps(
     2.6        imports: List[Name],
     2.7 -      keywords: List[(String, Option[(String, List[String])])],
     2.8 +      keywords: List[Outer_Syntax.Decl],
     2.9        uses: List[(String, Boolean)])
    2.10  
    2.11      object Name

     3.1 --- a/src/Pure/Thy/thy_header.scala	Thu Mar 15 09:55:42 2012 +0100
     3.2 +++ b/src/Pure/Thy/thy_header.scala	Thu Mar 15 10:16:21 2012 +0100
     3.3 @@ -113,7 +113,7 @@
     3.4  
     3.5  sealed case class Thy_Header(
     3.6    name: String, imports: List[String],
     3.7 -  keywords: List[(String, Option[(String, List[String])])],
     3.8 +  keywords: List[Outer_Syntax.Decl],
     3.9    uses: List[(String, Boolean)])
    3.10  {
    3.11    def map(f: String => String): Thy_Header =