src/Pure/Thy/thy_info.scala
changeset 66717 67dbf5cdc056
parent 66715 6bced18e2b91
child 66719 d37efafd55b5
     1.1 --- a/src/Pure/Thy/thy_info.scala	Fri Sep 29 17:41:39 2017 +0200
     1.2 +++ b/src/Pure/Thy/thy_info.scala	Fri Sep 29 20:49:42 2017 +0200
     1.3 @@ -53,8 +53,20 @@
     1.4      lazy val syntax: Outer_Syntax =
     1.5        resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
     1.6  
     1.7 -    def loaded_theories: Set[String] =
     1.8 -      resources.session_base.loaded_theories ++ rev_entries.map(_.name.theory)
     1.9 +    def loaded_theories: Graph[String, Outer_Syntax] =
    1.10 +      (resources.session_base.loaded_theories /: entries)({ case (graph, entry) =>
    1.11 +        val name = entry.name.theory
    1.12 +        val imports = entry.header.imports.map(p => p._1.theory)
    1.13 +
    1.14 +        if (graph.defined(name))
    1.15 +          error("Duplicate loaded theory entry " + quote(name))
    1.16 +
    1.17 +        for (dep <- imports if !graph.defined(dep))
    1.18 +          error("Missing loaded theory entry " + quote(dep) + " for " + quote(name))
    1.19 +
    1.20 +        val syntax = Outer_Syntax.merge(imports.map(graph.get_node(_))) + entry.header
    1.21 +        (graph.new_node(name, syntax) /: imports)((g, dep) => g.add_edge(dep, name))
    1.22 +      })
    1.23  
    1.24      def loaded_files: List[(String, List[Path])] =
    1.25      {