src/Pure/Isar/keyword.scala
changeset 63429 baedd4724f08
parent 63428 005b490f0ce2
child 63430 9c5fcd355a2d
     1.1 --- a/src/Pure/Isar/keyword.scala	Fri Jul 08 22:22:51 2016 +0200
     1.2 +++ b/src/Pure/Isar/keyword.scala	Sun Jul 10 11:18:35 2016 +0200
     1.3 @@ -88,6 +88,8 @@
     1.4  
     1.5    type Spec = ((String, List[String]), List[String])
     1.6  
     1.7 +  val no_spec: Spec = (("", Nil), Nil)
     1.8 +
     1.9    object Keywords
    1.10    {
    1.11      def empty: Keywords = new Keywords()
    1.12 @@ -130,21 +132,19 @@
    1.13  
    1.14      /* add keywords */
    1.15  
    1.16 -    def + (name: String): Keywords = new Keywords(minor + name, major, commands)
    1.17 -    def + (name: String, kind: String): Keywords = this + (name, (kind, Nil))
    1.18 -    def + (name: String, kind_tags: (String, List[String])): Keywords =
    1.19 -    {
    1.20 -      val major1 = major + name
    1.21 -      val commands1 = commands + (name -> kind_tags)
    1.22 -      new Keywords(minor, major1, commands1)
    1.23 -    }
    1.24 +    def + (name: String, kind: String = "", tags: List[String] = Nil): Keywords =
    1.25 +      if (kind == "") new Keywords(minor + name, major, commands)
    1.26 +      else {
    1.27 +        val major1 = major + name
    1.28 +        val commands1 = commands + (name -> (kind, tags))
    1.29 +        new Keywords(minor, major1, commands1)
    1.30 +      }
    1.31  
    1.32      def add_keywords(header: Thy_Header.Keywords): Keywords =
    1.33        (this /: header) {
    1.34 -        case (keywords, (name, None, _)) =>
    1.35 -          keywords + Symbol.decode(name) + Symbol.encode(name)
    1.36 -        case (keywords, (name, Some((kind_tags, _)), _)) =>
    1.37 -          keywords + (Symbol.decode(name), kind_tags) + (Symbol.encode(name), kind_tags)
    1.38 +        case (keywords, (name, ((kind, tags), _), _)) =>
    1.39 +          if (kind == "") keywords + Symbol.decode(name) + Symbol.encode(name)
    1.40 +          else keywords + (Symbol.decode(name), kind, tags) + (Symbol.encode(name), kind, tags)
    1.41        }
    1.42  
    1.43