src/Pure/Thy/thy_info.scala
changeset 66775 e8f27a35ee0f
parent 66743 ff05d922bc34
child 66776 b74b9d0bf763
     1.1 --- a/src/Pure/Thy/thy_info.scala	Fri Oct 06 21:33:33 2017 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.scala	Sat Oct 07 12:50:05 2017 +0200
     1.3 @@ -49,14 +49,13 @@
     1.4          val name = entry.name.theory
     1.5          val imports = entry.header.imports.map(p => p._1.theory)
     1.6  
     1.7 -        if (graph.defined(name))
     1.8 -          error("Duplicate loaded theory entry " + quote(name))
     1.9 +        val graph1 = (graph /: (name :: imports))(_.default_node(_, Thy_Header.bootstrap_syntax))
    1.10 +        val graph2 = (graph1 /: imports)(_.add_edge(_, name))
    1.11  
    1.12 -        for (dep <- imports if !graph.defined(dep))
    1.13 -          error("Missing loaded theory entry " + quote(dep) + " for " + quote(name))
    1.14 -
    1.15 -        val syntax = Outer_Syntax.merge(imports.map(graph.get_node(_))) + entry.header
    1.16 -        (graph.new_node(name, syntax) /: imports)((g, dep) => g.add_edge(dep, name))
    1.17 +        val syntax =
    1.18 +          Outer_Syntax.merge((name :: graph2.imm_preds(name).toList).map(graph2.get_node(_))) +
    1.19 +            entry.header
    1.20 +        graph2.map_node(name, _ => syntax)
    1.21        })
    1.22  
    1.23      def loaded_files: List[(String, List[Path])] =