# HG changeset patch
# User wenzelm
# Date 1506713431 -7200
# Node ID d37efafd55b5c30860c4a4fa8228a5060a35b835
# Parent  514c4907ff0bada9702a69691f18d81c12c76d94
clarified theory syntax vs. overall session syntax;

diff -r 514c4907ff0b -r d37efafd55b5 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Sep 29 21:03:04 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 21:30:31 2017 +0200
@@ -205,13 +205,13 @@
               resources.thy_info.dependencies(root_theories)
             }
 
-            val syntax = thy_deps.syntax
+            val session_syntax = thy_deps.overall_syntax
 
             val theory_files = thy_deps.names.map(_.path)
             val loaded_files =
               if (inlined_files) {
                 if (Sessions.is_pure(info.name)) {
-                  (Thy_Header.PURE -> resources.pure_files(syntax, info.dir)) ::
+                  (Thy_Header.PURE -> resources.pure_files(session_syntax, info.dir)) ::
                     thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
                 }
                 else thy_deps.loaded_files
@@ -226,8 +226,10 @@
             if (list_files)
               progress.echo(cat_lines(all_files.map(_.implode).sorted.map("  " + _)))
 
-            if (check_keywords.nonEmpty)
-              Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
+            if (check_keywords.nonEmpty) {
+              Check_Keywords.check_keywords(
+                progress, session_syntax.keywords, check_keywords, theory_files)
+            }
 
             val session_graph: Graph_Display.Graph =
             {
@@ -278,7 +280,7 @@
                 global_theories = global_theories,
                 loaded_theories = thy_deps.loaded_theories,
                 known = known,
-                syntax = syntax,
+                syntax = session_syntax,
                 sources = sources,
                 session_graph = session_graph,
                 errors = thy_deps.errors ::: sources_errors,
diff -r 514c4907ff0b -r d37efafd55b5 src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Fri Sep 29 21:03:04 2017 +0200
+++ b/src/Pure/Thy/thy_info.scala	Fri Sep 29 21:30:31 2017 +0200
@@ -26,34 +26,25 @@
 
   object Dependencies
   {
-    val empty = new Dependencies(Nil, Nil, Nil, Set.empty)
+    val empty = new Dependencies(Nil, Set.empty)
   }
 
   final class Dependencies private(
     rev_entries: List[Document.Node.Entry],
-    val keywords: Thy_Header.Keywords,
-    val abbrevs: Thy_Header.Abbrevs,
     val seen: Set[Document.Node.Name])
   {
     def :: (entry: Document.Node.Entry): Dependencies =
-      new Dependencies(
-        entry :: rev_entries,
-        entry.header.keywords ::: keywords,
-        entry.header.abbrevs ::: abbrevs,
-        seen)
+      new Dependencies(entry :: rev_entries, seen)
 
     def + (name: Document.Node.Name): Dependencies =
-      new Dependencies(rev_entries, keywords, abbrevs, seen + name)
+      new Dependencies(rev_entries, seen + name)
 
     def entries: List[Document.Node.Entry] = rev_entries.reverse
     def names: List[Document.Node.Name] = entries.map(_.name)
 
     def errors: List[String] = entries.flatMap(_.header.errors)
 
-    lazy val syntax: Outer_Syntax =
-      resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
-
-    def loaded_theories: Graph[String, Outer_Syntax] =
+    lazy val 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)
@@ -71,9 +62,13 @@
     def loaded_files: List[(String, List[Path])] =
     {
       names.map(_.theory) zip
-        Par_List.map((e: () => List[Path]) => e(), names.map(resources.loaded_files(syntax, _)))
+        Par_List.map((e: () => List[Path]) => e(),
+          names.map(name => resources.loaded_files(loaded_theories.get_node(name.theory), name)))
     }
 
+    lazy val overall_syntax: Outer_Syntax =
+      Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
+
     override def toString: String = entries.toString
   }