src/Pure/Isar/keyword.scala
changeset 59073 dcecfcc56dce
parent 58999 ed09ae4ea2d8
child 59122 c1dbcde94cd2
     1.1 --- a/src/Pure/Isar/keyword.scala	Mon Dec 01 14:24:05 2014 +0100
     1.2 +++ b/src/Pure/Isar/keyword.scala	Mon Dec 01 15:21:49 2014 +0100
     1.3 @@ -83,12 +83,8 @@
     1.4    class Keywords private(
     1.5      val minor: Scan.Lexicon = Scan.Lexicon.empty,
     1.6      val major: Scan.Lexicon = Scan.Lexicon.empty,
     1.7 -    commands: Map[String, (String, List[String])] = Map.empty)
     1.8 +    protected val commands: Map[String, (String, List[String])] = Map.empty)
     1.9    {
    1.10 -    /* content */
    1.11 -
    1.12 -    def is_empty: Boolean = minor.isEmpty && major.isEmpty
    1.13 -
    1.14      override def toString: String =
    1.15      {
    1.16        val keywords1 = minor.iterator.map(quote(_)).toList
    1.17 @@ -101,6 +97,24 @@
    1.18      }
    1.19  
    1.20  
    1.21 +    /* merge */
    1.22 +
    1.23 +    def is_empty: Boolean = minor.is_empty && major.is_empty
    1.24 +
    1.25 +    def ++ (other: Keywords): Keywords =
    1.26 +      if (this eq other) this
    1.27 +      else if (is_empty) other
    1.28 +      else {
    1.29 +        val minor1 = minor ++ other.minor
    1.30 +        val major1 = major ++ other.major
    1.31 +        val commands1 =
    1.32 +          if (commands eq other.commands) commands
    1.33 +          else if (commands.isEmpty) other.commands
    1.34 +          else (commands /: other.commands) { case (m, e) => if (m.isDefinedAt(e._1)) m else m + e }
    1.35 +        new Keywords(minor1, major1, commands1)
    1.36 +      }
    1.37 +
    1.38 +
    1.39      /* add keywords */
    1.40  
    1.41      def + (name: String): Keywords = new Keywords(minor + name, major, commands)