--- a/src/Pure/Isar/outer_syntax.scala Sat Oct 07 12:50:05 2017 +0200
+++ b/src/Pure/Isar/outer_syntax.scala Sat Oct 07 13:13:46 2017 +0200
@@ -18,9 +18,7 @@
def init(): Outer_Syntax = new Outer_Syntax(completion = Completion.init())
- def merge(syns: List[Outer_Syntax]): Outer_Syntax =
- if (syns.isEmpty) Thy_Header.bootstrap_syntax
- else (syns.head /: syns.tail)(_ ++ _)
+ def merge(syns: List[Outer_Syntax]): Outer_Syntax = (empty /: syns)(_ ++ _)
/* string literals */
@@ -109,6 +107,7 @@
def ++ (other: Outer_Syntax): Outer_Syntax =
if (this eq other) this
+ else if (this eq Outer_Syntax.empty) other
else {
val keywords1 = keywords ++ other.keywords
val completion1 = completion ++ other.completion