src/Pure/Isar/outer_syntax.scala
changeset 59077 7e0d3da6e6d8
parent 59073 dcecfcc56dce
child 59083 88b0b1f28adc
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Mon Dec 01 19:25:20 2014 +0100
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Tue Dec 02 14:16:56 2014 +0100
     1.3 @@ -114,12 +114,13 @@
     1.4  
     1.5    /* merge */
     1.6  
     1.7 -  def ++ (other: Outer_Syntax): Outer_Syntax =
     1.8 +  def ++ (other: Prover.Syntax): Prover.Syntax =
     1.9      if (this eq other) this
    1.10      else {
    1.11 -      val keywords1 = keywords ++ other.keywords
    1.12 -      val completion1 = completion ++ other.completion
    1.13 -      new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
    1.14 +      val keywords1 = keywords ++ other.asInstanceOf[Outer_Syntax].keywords
    1.15 +      val completion1 = completion ++ other.asInstanceOf[Outer_Syntax].completion
    1.16 +      if ((keywords eq keywords1) && (completion eq completion1)) this
    1.17 +      else new Outer_Syntax(keywords1, completion1, language_context, has_tokens)
    1.18      }
    1.19  
    1.20