src/Pure/Isar/outer_syntax.scala
changeset 66776 b74b9d0bf763
parent 66717 67dbf5cdc056
child 66983 df83b66f1d94
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Oct 07 12:50:05 2017 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Oct 07 13:13:46 2017 +0200
     1.3 @@ -18,9 +18,7 @@
     1.4  
     1.5    def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
     1.6  
     1.7 -  def merge(syns: List[Outer_Syntax]): Outer_Syntax =
     1.8 -    if (syns.isEmpty) Thy_Header.bootstrap_syntax
     1.9 -    else (syns.head /: syns.tail)(_ ++ _)
    1.10 +  def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _)
    1.11  
    1.12  
    1.13    /* string literals */
    1.14 @@ -109,6 +107,7 @@
    1.15  
    1.16    def ++ (other: Outer_Syntax): Outer_Syntax =
    1.17      if (this eq other) this
    1.18 +    else if (this eq Outer_Syntax.empty) other
    1.19      else {
    1.20        val keywords1 = keywords ++ other.keywords
    1.21        val completion1 = completion ++ other.completion