merged
authorwenzelm
Sat Oct 07 14:57:54 2017 +0200 (20 months ago)
changeset 667778df01b0db3e9
parent 66774 f90a1370cb6a
parent 66776 b74b9d0bf763
child 66778 cf0187ca3a57
merged
     1.1 --- a/src/Pure/Isar/outer_syntax.scala	Sat Oct 07 14:56:30 2017 +0200
     1.2 +++ b/src/Pure/Isar/outer_syntax.scala	Sat Oct 07 14:57:54 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
     2.1 --- a/src/Pure/Thy/thy_info.scala	Sat Oct 07 14:56:30 2017 +0200
     2.2 +++ b/src/Pure/Thy/thy_info.scala	Sat Oct 07 14:57:54 2017 +0200
     2.3 @@ -49,14 +49,14 @@
     2.4          val name = entry.name.theory
     2.5          val imports = entry.header.imports.map(p => p._1.theory)
     2.6  
     2.7 -        if (graph.defined(name))
     2.8 -          error("Duplicate loaded theory entry " + quote(name))
     2.9 +        val graph1 = (graph /: (name :: imports))(_.default_node(_, Outer_Syntax.empty))
    2.10 +        val graph2 = (graph1 /: imports)(_.add_edge(_, name))
    2.11  
    2.12 -        for (dep <- imports if !graph.defined(dep))
    2.13 -          error("Missing loaded theory entry " + quote(dep) + " for " + quote(name))
    2.14 +        val syntax0 = if (name == Thy_Header.PURE) List(Thy_Header.bootstrap_syntax) else Nil
    2.15 +        val syntax1 = (name :: graph2.imm_preds(name).toList).map(graph2.get_node(_))
    2.16 +        val syntax = Outer_Syntax.merge(syntax0 ::: syntax1) + entry.header
    2.17  
    2.18 -        val syntax = Outer_Syntax.merge(imports.map(graph.get_node(_))) + entry.header
    2.19 -        (graph.new_node(name, syntax) /: imports)((g, dep) => g.add_edge(dep, name))
    2.20 +        graph2.map_node(name, _ => syntax)
    2.21        })
    2.22  
    2.23      def loaded_files: List[(String, List[Path])] =