# HG changeset patch
# User wenzelm
# Date 1506717958 -7200
# Node ID 18cc87e2335f9087e6f3747b3b8dc0ae57a89b39
# Parent  676258a1cf01efab9d9755d361594637ceb7ee12# Parent  9c661b74ce9230b17e4379242b49fca76d320290
merged

diff -r 676258a1cf01 -r 18cc87e2335f NEWS
--- a/NEWS	Fri Sep 29 16:55:08 2017 +0100
+++ b/NEWS	Fri Sep 29 22:45:58 2017 +0200
@@ -7,6 +7,14 @@
 New in this Isabelle version
 ----------------------------
 
+*** General ***
+
+* Session-qualified theory names are mandatory: it is no longer possible
+to refer to unqualified theories from the parent session.
+INCOMPATIBILITY for old developments that have not been updated to
+Isabelle2017 yet (using the "isabelle imports" tool).
+
+
 *** HOL ***
 
 * SMT module:
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/Isar/outer_syntax.scala
--- a/src/Pure/Isar/outer_syntax.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Isar/outer_syntax.scala	Fri Sep 29 22:45:58 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 676258a1cf01 -r 18cc87e2335f src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/ML/ml_process.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -99,9 +99,11 @@
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
                 ML_Syntax.print_string, ML_Syntax.print_string))(table)
+          def print_list(list: List[String]): String =
+            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_table(base.loaded_theories.toList) +
+            ", loaded_theories = " + print_list(base.loaded_theories.keys) +
             ", known_theories = " + print_table(base.dest_known_theories) + "}")
       }
 
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/PIDE/document.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -116,6 +116,8 @@
           case _ => false
         }
 
+      def path: Path = Path.explode(node)
+
       def is_theory: Boolean = theory.nonEmpty
 
       def theory_base_name: String = Long_Name.base_name(theory)
@@ -126,6 +128,11 @@
       def map_theory(f: String => String): Name = copy(node, master_dir, f(theory))
     }
 
+    sealed case class Entry(name: Node.Name, header: Node.Header)
+    {
+      override def toString: String = name.toString
+    }
+
 
     /* node overlays */
 
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/PIDE/protocol.ML	Fri Sep 29 22:45:58 2017 +0200
@@ -22,10 +22,11 @@
     (fn [global_theories_yxml, loaded_theories_yxml, known_theories_yxml] =>
       let
         val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
+        val decode_list = YXML.parse_body #> let open XML.Decode in list string end;
       in
         Resources.init_session_base
           {global_theories = decode_table global_theories_yxml,
-           loaded_theories = decode_table loaded_theories_yxml,
+           loaded_theories = decode_list loaded_theories_yxml,
            known_theories = decode_table known_theories_yxml}
       end);
 
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/PIDE/protocol.scala
--- a/src/Pure/PIDE/protocol.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/PIDE/protocol.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -316,12 +316,18 @@
     Symbol.encode_yxml(list(pair(string, string))(table))
   }
 
+  private def encode_list(lst: List[String]): String =
+  {
+    import XML.Encode._
+    Symbol.encode_yxml(list(string)(lst))
+  }
+
   def session_base(resources: Resources)
   {
     val base = resources.session_base.standard_path
     protocol_command("Prover.session_base",
       encode_table(base.global_theories.toList),
-      encode_table(base.loaded_theories.toList),
+      encode_list(base.loaded_theories.keys),
       encode_table(base.dest_known_theories))
   }
 
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/PIDE/resources.ML	Fri Sep 29 22:45:58 2017 +0200
@@ -9,19 +9,18 @@
   val default_qualifier: string
   val init_session_base:
     {global_theories: (string * string) list,
-     loaded_theories: (string * string) list,
+     loaded_theories: string list,
      known_theories: (string * string) list} -> unit
   val finish_session_base: unit -> unit
   val global_theory: string -> string option
-  val loaded_theory: string -> string option
+  val loaded_theory: string -> bool
   val known_theory: string -> Path.T option
   val master_directory: theory -> Path.T
   val imports_of: theory -> (string * Position.T) list
   val begin_theory: Path.T -> Thy_Header.header -> theory list -> theory
   val thy_path: Path.T -> Path.T
   val theory_qualifier: string -> string
-  val import_name: string -> Path.T -> string ->
-    {node_name: Path.T, master_dir: Path.T, theory_name: string}
+  val import_name: string -> Path.T -> string -> {master_dir: Path.T, theory_name: string}
   val check_thy: Path.T -> string ->
    {master: Path.T * SHA1.digest, text: string, theory_pos: Position.T,
     imports: (string * Position.T) list, keywords: Thy_Header.keywords}
@@ -40,7 +39,7 @@
 
 val empty_session_base =
   {global_theories = Symtab.empty: string Symtab.table,
-   loaded_theories = Symtab.empty: string Symtab.table,
+   loaded_theories = Symtab.empty: unit Symtab.table,
    known_theories = Symtab.empty: Path.T Symtab.table};
 
 val global_session_base =
@@ -50,7 +49,7 @@
   Synchronized.change global_session_base
     (fn _ =>
       {global_theories = Symtab.make global_theories,
-       loaded_theories = Symtab.make loaded_theories,
+       loaded_theories = Symtab.make_set loaded_theories,
        known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
 
 fun finish_session_base () =
@@ -63,7 +62,7 @@
 fun get_session_base f = f (Synchronized.value global_session_base);
 
 fun global_theory a = Symtab.lookup (get_session_base #global_theories) a;
-fun loaded_theory a = Symtab.lookup (get_session_base #loaded_theories) a;
+fun loaded_theory a = Symtab.defined (get_session_base #loaded_theories) a;
 fun known_theory a = Symtab.lookup (get_session_base #known_theories) a;
 
 
@@ -108,26 +107,24 @@
     SOME qualifier => qualifier
   | NONE => Long_Name.qualifier theory);
 
-fun theory_name qualifier theory0 =
-  (case loaded_theory theory0 of
-    SOME theory => (true, theory)
-  | NONE =>
-      let val theory =
-        if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
-        then theory0
-        else Long_Name.qualify qualifier theory0
-      in (false, theory) end);
+fun theory_name qualifier theory =
+  if loaded_theory theory then (true, theory)
+  else
+    let val theory' =
+      if Long_Name.is_qualified theory orelse is_some (global_theory theory)
+      then theory
+      else Long_Name.qualify qualifier theory
+    in (false, theory') end;
 
 fun import_name qualifier dir s =
   (case theory_name qualifier (Thy_Header.import_name s) of
-    (true, theory) =>
-      {node_name = Path.basic theory, master_dir = Path.current, theory_name = theory}
+    (true, theory) => {master_dir = Path.current, theory_name = theory}
   | (false, theory) =>
       let val node_name =
         (case known_theory theory of
           SOME node_name => node_name
         | NONE => File.full_path dir (thy_path (Path.expand (Path.explode s))))
-      in {node_name = node_name, master_dir = Path.dir node_name, theory_name = theory} end);
+      in {master_dir = Path.dir node_name, theory_name = theory} end);
 
 fun check_file dir file = File.check_file (File.full_path dir file);
 
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/PIDE/resources.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -88,15 +88,14 @@
   def theory_qualifier(name: Document.Node.Name): String =
     session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
 
-  def theory_name(qualifier: String, theory0: String): (Boolean, String) =
-    session_base.loaded_theories.get(theory0) match {
-      case Some(theory) => (true, theory)
-      case None =>
-        val theory =
-          if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0))
-            theory0
-          else Long_Name.qualify(qualifier, theory0)
-        (false, theory)
+  def theory_name(qualifier: String, theory: String): (Boolean, String) =
+    if (session_base.loaded_theory(theory)) (true, theory)
+    else {
+      val theory1 =
+        if (Long_Name.is_qualified(theory) || session_base.global_theories.isDefinedAt(theory))
+          theory
+        else Long_Name.qualify(qualifier, theory)
+      (false, theory1)
     }
 
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
@@ -118,7 +117,7 @@
 
   def with_thy_reader[A](name: Document.Node.Name, f: Reader[Char] => A): A =
   {
-    val path = File.check_file(Path.explode(name.node))
+    val path = File.check_file(name.path)
     val reader = Scan.byte_reader(path.file)
     try { f(reader) } finally { reader.close }
   }
@@ -128,7 +127,7 @@
   {
     if (node_name.is_theory && reader.source.length > 0) {
       try {
-        val header = Thy_Header.read(reader, start, strict).decode_symbols
+        val header = Thy_Header.read(reader, start, strict)
 
         val base_name = node_name.theory_base_name
         val (name, pos) = header.name
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/PIDE/session.scala
--- a/src/Pure/PIDE/session.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/PIDE/session.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -220,7 +220,7 @@
 
   def recent_syntax(name: Document.Node.Name): Outer_Syntax =
     global_state.value.recent_finished.version.get_finished.nodes(name).syntax getOrElse
-    resources.session_base.syntax
+    resources.session_base.overall_syntax
 
 
   /* pipelined change parsing */
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Thy/sessions.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -40,8 +40,7 @@
       def local_theories_iterator =
       {
         val local_path = local_dir.canonical_file.toPath
-        theories.iterator.filter(name =>
-          Path.explode(name.node).canonical_file.toPath.startsWith(local_path))
+        theories.iterator.filter(name => name.path.canonical_file.toPath.startsWith(local_path))
       }
 
       val known_theories =
@@ -62,7 +61,7 @@
         (Map.empty[JFile, List[Document.Node.Name]] /:
             (bases_iterator(true) ++ bases_iterator(false) ++ theories.iterator))({
           case (known, name) =>
-            val file = Path.explode(name.node).canonical_file
+            val file = name.path.canonical_file
             val theories1 = known.getOrElse(file, Nil)
             if (theories1.exists(name1 => name.node == name1.node && name.theory == name1.theory))
               known
@@ -103,22 +102,18 @@
 
   object Base
   {
-    def pure(options: Options): Base = session_base(options, Thy_Header.PURE)
-
     def bootstrap(global_theories: Map[String, String]): Base =
       Base(
         global_theories = global_theories,
-        keywords = Thy_Header.bootstrap_header,
-        syntax = Thy_Header.bootstrap_syntax)
+        overall_syntax = Thy_Header.bootstrap_syntax)
   }
 
   sealed case class Base(
     pos: Position.T = Position.none,
     global_theories: Map[String, String] = Map.empty,
-    loaded_theories: Map[String, String] = Map.empty,
+    loaded_theories: Graph[String, Outer_Syntax] = Graph.string,
     known: Known = Known.empty,
-    keywords: Thy_Header.Keywords = Nil,
-    syntax: Outer_Syntax = Outer_Syntax.empty,
+    overall_syntax: Outer_Syntax = Outer_Syntax.empty,
     sources: List[(Path, SHA1.Digest)] = Nil,
     session_graph: Graph_Display.Graph = Graph_Display.empty_graph,
     errors: List[String] = Nil,
@@ -127,8 +122,16 @@
     def platform_path: Base = copy(known = known.platform_path)
     def standard_path: Base = copy(known = known.standard_path)
 
-    def loaded_theory(name: Document.Node.Name): Boolean =
-      loaded_theories.isDefinedAt(name.theory)
+    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 node_syntax(nodes: Document.Nodes, name: Document.Node.Name): Option[Outer_Syntax] =
+      nodes(name).syntax orElse loaded_theory_syntax(name)
 
     def known_theory(name: String): Option[Document.Node.Name] =
       known.theories.get(name)
@@ -203,13 +206,13 @@
               resources.thy_info.dependencies(root_theories)
             }
 
-            val syntax = thy_deps.syntax
+            val overall_syntax = thy_deps.overall_syntax
 
-            val theory_files = thy_deps.deps.map(dep => Path.explode(dep.name.node))
+            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(overall_syntax, info.dir)) ::
                     thy_deps.loaded_files.filterNot(p => p._1 == Thy_Header.PURE)
                 }
                 else thy_deps.loaded_files
@@ -224,8 +227,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, overall_syntax.keywords, check_keywords, theory_files)
+            }
 
             val session_graph: Graph_Display.Graph =
             {
@@ -251,18 +256,18 @@
                       val bs = imports_subgraph.imm_preds(session).toList.map(session_node(_))
                       ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
 
-              (graph0 /: thy_deps.deps)(
-                { case (g, dep) =>
-                    val a = node(dep.name)
+              (graph0 /: thy_deps.entries)(
+                { case (g, entry) =>
+                    val a = node(entry.name)
                     val bs =
-                      dep.header.imports.map({ case (name, _) => node(name) }).
+                      entry.header.imports.map({ case (name, _) => node(name) }).
                         filterNot(_ == a)
                     ((g /: (a :: bs))(_.default_node(_, Nil)) /: bs)(_.add_edge(_, a)) })
             }
 
             val known =
               Known.make(info.dir, List(imports_base),
-                theories = thy_deps.deps.map(_.name),
+                theories = thy_deps.names,
                 loaded_files = loaded_files)
 
             val sources =
@@ -276,8 +281,7 @@
                 global_theories = global_theories,
                 loaded_theories = thy_deps.loaded_theories,
                 known = known,
-                keywords = thy_deps.keywords,
-                syntax = syntax,
+                overall_syntax = overall_syntax,
                 sources = sources,
                 session_graph = session_graph,
                 errors = thy_deps.errors ::: sources_errors,
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Thy/thy_header.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -138,7 +138,14 @@
       (opt($$$(ABBREVS) ~! abbrevs) ^^
         { case None => Nil case Some(_ ~ xs) => xs }) ~
       $$$(BEGIN) ^^
-      { case x ~ ys ~ zs ~ ws ~ _ => Thy_Header(x, ys, zs, ws) }
+      { case (name, pos) ~ imports ~ keywords ~ abbrevs ~ _ =>
+          val f = Symbol.decode _
+          Thy_Header((f(name), pos),
+            imports.map({ case (a, b) => (f(a), b) }),
+            keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
+              (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
+            abbrevs.map({ case (a, b) => (f(a), f(b)) }))
+      }
 
     val heading =
       (command(CHAPTER) |
@@ -197,20 +204,8 @@
   }
 }
 
-
 sealed case class Thy_Header(
   name: (String, Position.T),
   imports: List[(String, Position.T)],
   keywords: Thy_Header.Keywords,
   abbrevs: Thy_Header.Abbrevs)
-{
-  def decode_symbols: Thy_Header =
-  {
-    val f = Symbol.decode _
-    Thy_Header((f(name._1), name._2),
-      imports.map({ case (a, b) => (f(a), b) }),
-      keywords.map({ case (a, Keyword.Spec(b, c, d)) =>
-        (f(a), Keyword.Spec(f(b), c.map(f), d.map(f))) }),
-      abbrevs.map({ case (a, b) => (f(a), f(b)) }))
-  }
-}
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/Thy/thy_info.ML
--- a/src/Pure/Thy/thy_info.ML	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Thy/thy_info.ML	Fri Sep 29 22:45:58 2017 +0200
@@ -160,7 +160,7 @@
   in res :: map Exn.Exn exns end;
 
 datatype task =
-  Task of Path.T * string list * (theory list -> result) |
+  Task of string list * (theory list -> result) |
   Finished of theory;
 
 fun task_finished (Task _) = false
@@ -171,7 +171,7 @@
 val schedule_seq =
   String_Graph.schedule (fn deps => fn (_, task) =>
     (case task of
-      Task (_, parents, body) =>
+      Task (parents, body) =>
         let
           val result = body (task_parents deps parents);
           val _ = Par_Exn.release_all (join_theory result);
@@ -185,7 +185,7 @@
     val futures = tasks
       |> String_Graph.schedule (fn deps => fn (name, task) =>
         (case task of
-          Task (_, parents, body) =>
+          Task (parents, body) =>
             (singleton o Future.forks)
               {name = "theory:" ^ name, group = NONE,
                 deps = map (Future.task_of o #2) deps, pri = 0, interrupts = true}
@@ -335,19 +335,10 @@
       |>> forall I
 and require_thy document symbols last_timing initiators qualifier dir (s, require_pos) tasks =
   let
-    val {node_name, master_dir, theory_name} = Resources.import_name qualifier dir s;
-    fun check_entry (Task (node_name', _, _)) =
-          if op = (apply2 File.platform_path (node_name, node_name'))
-          then ()
-          else
-            error ("Incoherent imports for theory " ^ quote theory_name ^
-              Position.here require_pos ^ ":\n" ^
-              "  " ^ Path.print node_name ^ "\n" ^
-              "  " ^ Path.print node_name')
-      | check_entry _ = ();
+    val {master_dir, theory_name, ...} = Resources.import_name qualifier dir s;
   in
     (case try (String_Graph.get_node tasks) theory_name of
-      SOME task => (check_entry task; (task_finished task, tasks))
+      SOME task => (task_finished task, tasks)
     | NONE =>
         let
           val _ = member (op =) initiators theory_name andalso error (cycle_msg initiators);
@@ -378,7 +369,7 @@
                     val load =
                       load_thy document symbols last_timing initiators update_time dep
                         text (theory_name, theory_pos) keywords;
-                  in Task (node_name, parents, load) end);
+                  in Task (parents, load) end);
 
           val tasks'' = new_entry theory_name parents task tasks';
         in (all_current, tasks'') end)
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/Thy/thy_info.scala
--- a/src/Pure/Thy/thy_info.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Thy/thy_info.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -7,18 +7,6 @@
 package isabelle
 
 
-object Thy_Info
-{
-  /* dependencies */
-
-  sealed case class Dep(
-    name: Document.Node.Name,
-    header: Document.Node.Header)
-  {
-    override def toString: String = name.toString
-  }
-}
-
 class Thy_Info(resources: Resources)
 {
   /* messages */
@@ -38,64 +26,50 @@
 
   object Dependencies
   {
-    val empty = new Dependencies(Nil, Nil, Nil, Set.empty, Multi_Map.empty)
+    val empty = new Dependencies(Nil, Set.empty)
   }
 
   final class Dependencies private(
-    rev_deps: List[Thy_Info.Dep],
-    val keywords: Thy_Header.Keywords,
-    val abbrevs: Thy_Header.Abbrevs,
-    val seen: Set[Document.Node.Name],
-    val seen_theory: Multi_Map[String, (Document.Node.Name, Position.T)])
+    rev_entries: List[Document.Node.Entry],
+    val seen: Set[Document.Node.Name])
   {
-    def :: (dep: Thy_Info.Dep): Dependencies =
-      new Dependencies(
-        dep :: rev_deps, dep.header.keywords ::: keywords, dep.header.abbrevs ::: abbrevs,
-        seen, seen_theory)
+    def :: (entry: Document.Node.Entry): Dependencies =
+      new Dependencies(entry :: rev_entries, seen)
 
-    def + (thy: (Document.Node.Name, Position.T)): Dependencies =
-    {
-      val (name, _) = thy
-      new Dependencies(rev_deps, keywords, abbrevs, seen + name, seen_theory + (name.theory -> thy))
-    }
+    def + (name: Document.Node.Name): Dependencies =
+      new Dependencies(rev_entries, seen + name)
 
-    def deps: List[Thy_Info.Dep] = rev_deps.reverse
+    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)
 
-    def errors: List[String] =
-    {
-      val header_errors = deps.flatMap(dep => dep.header.errors)
-      val import_errors =
-        (for {
-          (theory, imports) <- seen_theory.iterator_list
-          if !resources.session_base.loaded_theories.isDefinedAt(theory)
-          if imports.length > 1
-        } yield {
-          "Incoherent imports for theory " + quote(theory) + ":\n" +
-            cat_lines(imports.map({ case (name, pos) =>
-              "  " + quote(name.node) + Position.here(pos) }))
-        }).toList
-      header_errors ::: import_errors
-    }
+    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)
 
-    lazy val syntax: Outer_Syntax =
-      resources.session_base.syntax.add_keywords(keywords).add_abbrevs(abbrevs)
+        if (graph.defined(name))
+          error("Duplicate loaded theory entry " + quote(name))
 
-    def loaded_theories: Map[String, String] =
-      (resources.session_base.loaded_theories /: rev_deps) {
-        case (loaded, dep) =>
-          val name = dep.name
-          loaded + (name.theory -> name.theory) +
-            (name.theory_base_name -> name.theory)  // legacy
-      }
+        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])] =
     {
-      val names = deps.map(_.name)
       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)))
     }
 
-    override def toString: String = deps.toString
+    lazy val overall_syntax: Outer_Syntax =
+      Outer_Syntax.merge(loaded_theories.maximals.map(loaded_theories.get_node(_)))
+
+    override def toString: String = entries.toString
   }
 
   private def require_thys(initiators: List[Document.Node.Name], required: Dependencies,
@@ -105,13 +79,13 @@
   private def require_thy(initiators: List[Document.Node.Name], required: Dependencies,
     thy: (Document.Node.Name, Position.T)): Dependencies =
   {
-    val (name, require_pos) = thy
+    val (name, pos) = thy
 
     def message: String =
       "The error(s) above occurred for theory " + quote(name.theory) +
-        required_by(initiators) + Position.here(require_pos)
+        required_by(initiators) + Position.here(pos)
 
-    val required1 = required + thy
+    val required1 = required + name
     if (required.seen(name)) required
     else if (resources.session_base.loaded_theory(name)) required1
     else {
@@ -120,11 +94,12 @@
         val header =
           try { resources.check_thy(name, Token.Pos.file(name.node)).cat_errors(message) }
           catch { case ERROR(msg) => cat_error(msg, message) }
-        Thy_Info.Dep(name, header) :: require_thys(name :: initiators, required1, header.imports)
+        Document.Node.Entry(name, header) ::
+          require_thys(name :: initiators, required1, header.imports)
       }
       catch {
         case e: Throwable =>
-          Thy_Info.Dep(name, Document.Node.bad_header(Exn.message(e))) :: required1
+          Document.Node.Entry(name, Document.Node.bad_header(Exn.message(e))) :: required1
       }
     }
   }
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/Thy/thy_syntax.scala
--- a/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Thy/thy_syntax.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -100,9 +100,10 @@
         if (node.is_empty) None
         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))
+          val imports_syntax =
+            Outer_Syntax.merge(
+              header.imports.flatMap(p => resources.session_base.node_syntax(nodes, p._1)))
+          Some(imports_syntax + header)
         }
       nodes += (name -> node.update_syntax(syntax))
     }
@@ -324,7 +325,9 @@
         node_edits foreach {
           case (name, edits) =>
             val node = nodes(name)
-            val syntax = node.syntax getOrElse resources.session_base.syntax
+            val syntax =
+              resources.session_base.node_syntax(nodes, name) getOrElse
+              Thy_Header.bootstrap_syntax
             val commands = node.commands
 
             val node1 =
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Tools/build.ML	Fri Sep 29 22:45:58 2017 +0200
@@ -147,7 +147,7 @@
   master_dir: Path.T,
   theories: (Options.T * (string * Position.T) list) list,
   global_theories: (string * string) list,
-  loaded_theories: (string * string) list,
+  loaded_theories: string list,
   known_theories: (string * string) list};
 
 fun decode_args yxml =
@@ -162,7 +162,7 @@
           (pair string
             (pair (((list (pair Options.decode (list (pair string position))))))
               (pair (list (pair string string))
-                (pair (list (pair string string)) (list (pair string string)))))))))))))))
+                (pair (list string) (list (pair string string)))))))))))))))
       (YXML.parse_body yxml);
   in
     Args {symbol_codes = symbol_codes, command_timings = command_timings, do_output = do_output,
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Tools/build.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -209,13 +209,13 @@
                 pair(Path.encode, pair(list(pair(Path.encode, Path.encode)), pair(string,
                 pair(string, pair(string, pair(string, pair(Path.encode,
                 pair(list(pair(Options.encode, list(pair(string, properties)))),
-                pair(list(pair(string, string)), pair(list(pair(string, string)),
+                pair(list(pair(string, string)), pair(list(string),
                 list(pair(string, string))))))))))))))))(
               (Symbol.codes, (command_timings, (do_output, (verbose,
                 (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)))))))))))))))
             })
 
diff -r 676258a1cf01 -r 18cc87e2335f src/Pure/Tools/imports.scala
--- a/src/Pure/Tools/imports.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Pure/Tools/imports.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -105,7 +105,7 @@
           (for {
             (_, a) <- session_resources.session_base.known.theories.iterator
             if session_resources.theory_qualifier(a) == info.theory_qualifier
-            b <- deps.all_known.get_file(Path.explode(a.node).file)
+            b <- deps.all_known.get_file(a.path.file)
             qualifier = session_resources.theory_qualifier(b)
             if !declared_imports.contains(qualifier)
           } yield qualifier).toSet
@@ -146,7 +146,7 @@
             val s1 =
               if (imports_base.loaded_theory(name)) name.theory
               else {
-                imports_base.known.get_file(Path.explode(name.node).file) match {
+                imports_base.known.get_file(name.path.file) match {
                   case Some(name1) if session_resources.theory_qualifier(name1) != qualifier =>
                     name1.theory
                   case Some(name1) if Thy_Header.is_base_name(s) =>
@@ -170,7 +170,7 @@
               (_, name) <- session_base.known.theories_local.toList
               if session_resources.theory_qualifier(name) == info.theory_qualifier
               (_, pos) <- session_resources.check_thy(name, Token.Pos.file(name.node)).imports
-              upd <- update_name(session_base.syntax.keywords, pos,
+              upd <- update_name(session_base.overall_syntax.keywords, pos,
                 standard_import(session_resources.theory_qualifier(name), name.master_dir, _))
             } yield upd
 
diff -r 676258a1cf01 -r 18cc87e2335f src/Tools/VSCode/src/build_vscode.scala
--- a/src/Tools/VSCode/src/build_vscode.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Tools/VSCode/src/build_vscode.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -20,7 +20,7 @@
   def build_grammar(options: Options, progress: Progress = No_Progress)
   {
     val logic = Grammar.default_logic
-    val keywords = Sessions.session_base(options, logic).syntax.keywords
+    val keywords = Sessions.session_base(options, logic).overall_syntax.keywords
 
     val output_path = extension_dir + Path.explode(Grammar.default_output(logic))
     progress.echo(output_path.implode)
diff -r 676258a1cf01 -r 18cc87e2335f src/Tools/VSCode/src/grammar.scala
--- a/src/Tools/VSCode/src/grammar.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Tools/VSCode/src/grammar.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -157,7 +157,7 @@
     val more_args = getopts(args)
     if (more_args.nonEmpty) getopts.usage()
 
-    val keywords = Sessions.session_base(Options.init(), logic, dirs).syntax.keywords
+    val keywords = Sessions.session_base(Options.init(), logic, dirs).overall_syntax.keywords
     val output_path = output getOrElse Path.explode(default_output(logic))
 
     Output.writeln(output_path.implode)
diff -r 676258a1cf01 -r 18cc87e2335f src/Tools/VSCode/src/vscode_resources.scala
--- a/src/Tools/VSCode/src/vscode_resources.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Tools/VSCode/src/vscode_resources.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -216,7 +216,7 @@
           (for ((_, model) <- st.models.iterator if model.is_theory)
            yield (model.node_name, Position.none)).toList
 
-        val thy_files = thy_info.dependencies(thys).deps.map(_.name)
+        val thy_files = thy_info.dependencies(thys).names
 
 
         /* auxiliary files */
diff -r 676258a1cf01 -r 18cc87e2335f src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -253,7 +253,7 @@
               val pending_nodes = for ((node_name, None) <- purged) yield node_name
               (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
             }
-            val retain = PIDE.resources.thy_info.dependencies(imports).deps.map(_.name).toSet
+            val retain = PIDE.resources.thy_info.dependencies(imports).names.toSet
 
             for ((node_name, Some(edits)) <- purged; if !retain(node_name); edit <- edits)
               yield edit
diff -r 676258a1cf01 -r 18cc87e2335f src/Tools/jEdit/src/isabelle.scala
--- a/src/Tools/jEdit/src/isabelle.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Tools/jEdit/src/isabelle.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -50,7 +50,7 @@
 
   def mode_syntax(mode: String): Option[Outer_Syntax] =
     mode match {
-      case "isabelle" => Some(PIDE.resources.session_base.syntax)
+      case "isabelle" => Some(PIDE.resources.session_base.overall_syntax)
       case "isabelle-options" => Some(Options.options_syntax)
       case "isabelle-root" => Some(Sessions.root_syntax)
       case "isabelle-ml" => Some(ml_syntax)
diff -r 676258a1cf01 -r 18cc87e2335f src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Fri Sep 29 16:55:08 2017 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Fri Sep 29 22:45:58 2017 +0200
@@ -126,7 +126,7 @@
           val thys =
             (for ((node_name, model) <- models.iterator if model.is_theory)
               yield (node_name, Position.none)).toList
-          val thy_files = resources.thy_info.dependencies(thys).deps.map(_.name)
+          val thy_files = resources.thy_info.dependencies(thys).names
 
           val aux_files =
             if (options.bool("jedit_auto_resolve")) {