src/Pure/Isar/outer_syntax.scala
changeset 48706 e2b512024eab
parent 48671 951bc4c3ee17
child 48707 ba531af91148
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Aug 07 12:35:24 2012 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Aug 07 13:21:29 2012 +0200
     1.3 @@ -34,8 +34,6 @@
     1.4      result.toString
     1.5    }
     1.6  
     1.7 -  type Decl = (String, Option[(String, List[String])])
     1.8 -
     1.9    val empty: Outer_Syntax = new Outer_Syntax()
    1.10    def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
    1.11  }
    1.12 @@ -61,10 +59,15 @@
    1.13  
    1.14    def + (name: String, kind: String): Outer_Syntax = this + (name, kind, name)
    1.15    def + (name: String): Outer_Syntax = this + (name, Keyword.MINOR)
    1.16 -  def + (decl: Outer_Syntax.Decl): Outer_Syntax =
    1.17 -    decl match {
    1.18 -      case ((name, Some((kind, _)))) => this + (name, kind)
    1.19 -      case ((name, None)) => this + name
    1.20 +
    1.21 +  def add_keywords(header: Document.Node_Header): Outer_Syntax =
    1.22 +    header match {
    1.23 +      case Exn.Res(deps) =>
    1.24 +        (this /: deps.keywords) {
    1.25 +          case (syntax, ((name, Some((kind, _))))) => syntax + (name, kind)
    1.26 +          case (syntax, ((name, None))) => syntax + name
    1.27 +        }
    1.28 +      case Exn.Exn(_) => this
    1.29      }
    1.30  
    1.31    def is_command(name: String): Boolean =