src/Pure/Isar/outer_syntax.scala
changeset 66717 67dbf5cdc056
parent 65384 36255c43c64c
child 66776 b74b9d0bf763
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Fri Sep 29 17:41:39 2017 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Fri Sep 29 20:49:42 2017 +0200
     1.3 @@ -18,6 +18,10 @@
     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 +
    1.11  
    1.12    /* string literals */
    1.13  
    1.14 @@ -98,7 +102,10 @@
    1.15      }
    1.16  
    1.17  
    1.18 -  /* merge */
    1.19 +  /* build */
    1.20 +
    1.21 +  def + (header: Document.Node.Header): Outer_Syntax =
    1.22 +    add_keywords(header.keywords).add_abbrevs(header.abbrevs)
    1.23  
    1.24    def ++ (other: Outer_Syntax): Outer_Syntax =
    1.25      if (this eq other) this