proper name according to meaning;
authorwenzelm
Tue Apr 04 22:53:01 2017 +0200 (2017-04-04)
changeset 65383089f2edefb77
parent 65382 de848ac5e0d7
child 65384 36255c43c64c
proper name according to meaning;
src/Pure/Isar/outer_syntax.scala
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Tue Apr 04 22:16:42 2017 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Apr 04 22:53:01 2017 +0200
     1.3 @@ -57,9 +57,9 @@
     1.4  
     1.5    /* keywords */
     1.6  
     1.7 -  def + (name: String, kind: String = "", tags: List[String] = Nil): Outer_Syntax =
     1.8 +  def + (name: String, kind: String = "", exts: List[String] = Nil): Outer_Syntax =
     1.9    {
    1.10 -    val keywords1 = keywords + (name, kind, tags)
    1.11 +    val keywords1 = keywords + (name, kind, exts)
    1.12      val completion1 =
    1.13        completion.add_keyword(name).
    1.14          add_abbrevs(
    1.15 @@ -71,8 +71,8 @@
    1.16  
    1.17    def add_keywords(keywords: Thy_Header.Keywords): Outer_Syntax =
    1.18      (this /: keywords) {
    1.19 -      case (syntax, (name, ((kind, tags), _))) =>
    1.20 -        syntax + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
    1.21 +      case (syntax, (name, ((kind, exts), _))) =>
    1.22 +        syntax + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
    1.23      }
    1.24  
    1.25