src/Pure/Isar/outer_syntax.scala
changeset 63429 baedd4724f08
parent 63424 e4e15bbfb3e2
child 63441 4c3fa4dba79f
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Fri Jul 08 22:22:51 2016 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sun Jul 10 11:18:35 2016 +0200
     1.3 @@ -85,16 +85,10 @@
     1.4  
     1.5    /* add keywords */
     1.6  
     1.7 -  def + (name: String): Outer_Syntax = this + (name, None, None)
     1.8 -  def + (name: String, kind: String): Outer_Syntax = this + (name, Some((kind, Nil)), None)
     1.9 -  def + (name: String, opt_kind: Option[(String, List[String])], replace: Option[String])
    1.10 +  def + (name: String, kind: String = "", tags: List[String] = Nil, replace: Option[String] = None)
    1.11      : Outer_Syntax =
    1.12    {
    1.13 -    val keywords1 =
    1.14 -      opt_kind match {
    1.15 -        case None => keywords + name
    1.16 -        case Some(kind) => keywords + (name, kind)
    1.17 -      }
    1.18 +    val keywords1 = keywords + (name, kind, tags)
    1.19      val completion1 =
    1.20        if (replace == Some("")) completion
    1.21        else completion + (name, replace getOrElse name)
    1.22 @@ -103,11 +97,10 @@
    1.23  
    1.24    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    1.25      (this /: keywords) {
    1.26 -      case (syntax, (name, opt_spec, replace)) =>
    1.27 -        val opt_kind = opt_spec.map(_._1)
    1.28 +      case (syntax, (name, ((kind, tags), _), replace)) =>
    1.29          syntax +
    1.30 -          (Symbol.decode(name), opt_kind, replace) +
    1.31 -          (Symbol.encode(name), opt_kind, replace)
    1.32 +          (Symbol.decode(name), kind, tags, replace) +
    1.33 +          (Symbol.encode(name), kind, tags, replace)
    1.34      }
    1.35  
    1.36