src/Pure/Isar/keyword.scala
changeset 65384 36255c43c64c
parent 63809 56670ab6f55e
child 65385 23f36ab9042b
     1.1 --- a/src/Pure/Isar/keyword.scala	Tue Apr 04 22:53:01 2017 +0200
     1.2 +++ b/src/Pure/Isar/keyword.scala	Tue Apr 04 22:56:28 2017 +0200
     1.3 @@ -93,11 +93,14 @@
     1.4  
     1.5    /** keyword tables **/
     1.6  
     1.7 -  type Spec = ((String, List[String]), List[String])
     1.8 -
     1.9 -  val no_spec: Spec = (("", Nil), Nil)
    1.10 -  val before_command_spec: Spec = ((BEFORE_COMMAND, Nil), Nil)
    1.11 -  val quasi_command_spec: Spec = ((QUASI_COMMAND, Nil), Nil)
    1.12 +  object Spec
    1.13 +  {
    1.14 +    val none: Spec = Spec("")
    1.15 +  }
    1.16 +  sealed case class Spec(kind: String, exts: List[String] = Nil, tags: List[String] = Nil)
    1.17 +  {
    1.18 +    def is_none: Boolean = kind == ""
    1.19 +  }
    1.20  
    1.21    object Keywords
    1.22    {
    1.23 @@ -165,9 +168,13 @@
    1.24  
    1.25      def add_keywords(header: Thy_Header.Keywords): Keywords =
    1.26        (this /: header) {
    1.27 -        case (keywords, (name, ((kind, exts), _))) =>
    1.28 -          if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
    1.29 -          else keywords + (Symbol.decode(name), kind, exts) + (Symbol.encode(name), kind, exts)
    1.30 +        case (keywords, (name, spec)) =>
    1.31 +          if (spec.is_none)
    1.32 +            keywords + Symbol.decode(name) + Symbol.encode(name)
    1.33 +          else
    1.34 +            keywords +
    1.35 +              (Symbol.decode(name), spec.kind, spec.exts) +
    1.36 +              (Symbol.encode(name), spec.kind, spec.exts)
    1.37        }
    1.38  
    1.39