src/Pure/Isar/outer_syntax.scala
changeset 59073 dcecfcc56dce
parent 58938 0c45680b7d9d
child 59077 7e0d3da6e6d8
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Dec 01 14:24:05 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Mon Dec 01 15:21:49 2014 +0100
     1.3 @@ -112,6 +112,17 @@
     1.4      }
     1.5  
     1.6  
     1.7 +  /* merge */
     1.8 +
     1.9 +  def ++ (other: Outer_Syntax): Outer_Syntax =
    1.10 +    if (this eq other) this
    1.11 +    else {
    1.12 +      val keywords1 = keywords ++ other.keywords
    1.13 +      val completion1 = completion ++ other.completion
    1.14 +      new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
    1.15 +    }
    1.16 +
    1.17 +
    1.18    /* load commands */
    1.19  
    1.20    def load_command(name: String): Option[List[String]] = keywords.load_command(name)