# HG changeset patch
# User wenzelm
# Date 1506710982 -7200
# Node ID 67dbf5cdc056ad50be43e78348e8d8d083866442
# Parent  8737b866bd1ce5890d1e29c35ad932bcfb6c0b86
more informative loaded_theories: dependencies and syntax;

diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Fri Sep 29 17:41:39 2017 +0200
+++ b/src/Pure/Isar/outer_syntax.scala	Fri Sep 29 20:49:42 2017 +0200
@@ -18,6 +18,10 @@
 
   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)(_ ++ _)
+
 
   /* string literals */
 
@@ -98,7 +102,10 @@
     }
 
 
-  /* merge */
+  /* build */
+
+  def + (header: Document.Node.Header): Outer_Syntax =
+    add_keywords(header.keywords).add_abbrevs(header.abbrevs)
 
   def ++ (other: Outer_Syntax): Outer_Syntax =
     if (this eq other) this
diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Fri Sep 29 17:41:39 2017 +0200
+++ b/src/Pure/ML/ml_process.scala	Fri Sep 29 20:49:42 2017 +0200
@@ -103,7 +103,7 @@
             ML_Syntax.print_list(ML_Syntax.print_string)(list)
           List("Resources.init_session_base" +
             " {global_theories = " + print_table(base.global_theories.toList) +
-            ", loaded_theories = " + print_list(base.loaded_theories.toList) +
+            ", loaded_theories = " + print_list(base.loaded_theories.keys) +
             ", known_theories = " + print_table(base.dest_known_theories) + "}")
       }
 
diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Sep 29 17:41:39 2017 +0200
+++ b/src/Pure/PIDE/protocol.scala	Fri Sep 29 20:49:42 2017 +0200
@@ -327,7 +327,7 @@
     val base = resources.session_base.standard_path
     protocol_command("Prover.session_base",
       encode_table(base.global_theories.toList),
-      encode_list(base.loaded_theories.toList),
+      encode_list(base.loaded_theories.keys),
       encode_table(base.dest_known_theories))
   }
 
diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Sep 29 17:41:39 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 20:49:42 2017 +0200
@@ -114,7 +114,7 @@
   sealed case class Base(
     pos: Position.T = Position.none,
     global_theories: Map[String, String] = Map.empty,
-    loaded_theories: Set[String] = Set.empty,
+    loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     known: Known = Known.empty,
     keywords: Thy_Header.Keywords = Nil,
     syntax: Outer_Syntax = Outer_Syntax.empty,
@@ -126,9 +126,14 @@
     def platform_path: Base = copy(known = known.platform_path)
     def standard_path: Base = copy(known = known.standard_path)
 
-    def loaded_theory(name: String): Boolean = loaded_theories.contains(name)
+    def loaded_theory(name: String): Boolean = loaded_theories.defined(name)
     def loaded_theory(name: Document.Node.Name): Boolean = loaded_theory(name.theory)
 
+    def loaded_theory_syntax(name: String): Option[Outer_Syntax] =
+      if (loaded_theory(name)) Some(loaded_theories.get_node(name)) else None
+    def loaded_theory_syntax(name: Document.Node.Name): Option[Outer_Syntax] =
+      loaded_theory_syntax(name.theory)
+
     def known_theory(name: String): Option[Document.Node.Name] =
       known.theories.get(name)
 
diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Fri Sep 29 17:41:39 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Fri Sep 29 20:49:42 2017 +0200
@@ -53,8 +53,20 @@
     lazy val syntax: Outer_Syntax =
       resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
 
-    def loaded_theories: Set[String] =
-      resources.session_base.loaded_theories ++ rev_entries.map(_.name.theory)
+    def loaded_theories: Graph[String, Outer_Syntax] =
+      (resources.session_base.loaded_theories /: entries)({ case (graph, entry) =>
+        val name = entry.name.theory
+        val imports = entry.header.imports.map(p => p._1.theory)
+
+        if (graph.defined(name))
+          error("Duplicate loaded theory entry " + quote(name))
+
+        for (dep <- imports if !graph.defined(dep))
+          error("Missing loaded theory entry " + quote(dep) + " for " + quote(name))
+
+        val syntax = Outer_Syntax.merge(imports.map(graph.get_node(_))) + entry.header
+        (graph.new_node(name, syntax) /: imports)((g, dep) => g.add_edge(dep, name))
+      })
 
     def loaded_files: List[(String, List[Path])] =
     {
diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 17:41:39 2017 +0200
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 20:49:42 2017 +0200
@@ -101,8 +101,7 @@
         else {
           val header = node.header
           val imports_syntax = header.imports.flatMap(a => nodes(a._1).syntax)
-          Some((resources.session_base.syntax /: imports_syntax)(_ ++ _)
-            .add_keywords(header.keywords).add_abbrevs(header.abbrevs))
+          Some((resources.session_base.syntax /: imports_syntax)(_ ++ _) + header)
         }
       nodes += (name -> node.update_syntax(syntax))
     }
diff -r 8737b866bd1c -r 67dbf5cdc056 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Sep 29 17:41:39 2017 +0200
+++ b/src/Pure/Tools/build.scala	Fri Sep 29 20:49:42 2017 +0200
@@ -215,7 +215,7 @@
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
                 (parent, (info.chapter, (name, (Path.current,
                 (info.theories,
-                (base.global_theories.toList, (base.loaded_theories.toList,
+                (base.global_theories.toList, (base.loaded_theories.keys,
                 base.dest_known_theories)))))))))))))))
             })