# HG changeset patch
# User wenzelm
# Date 1491327647 -7200
# Node ID b722ee40c26c1a637e510cf6d096e62246e73869
# Parent  ce09e947c1d50e490e1e417287ccdfd77761d678
refer to global_theories from all sessions, before selection;

diff -r ce09e947c1d5 -r b722ee40c26c src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Tue Apr 04 18:43:58 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Tue Apr 04 19:40:47 2017 +0200
@@ -67,12 +67,16 @@
     }
     else Nil
 
-  def init_name(global: Boolean, raw_path: Path): Document.Node.Name =
+  def qualify(name: String): String =
+    if (Long_Name.is_qualified(name)) error("Bad qualified theory name " + quote(name))
+    else if (session_base.global_theories.contains(name)) name
+    else Long_Name.qualify(session_name, name)
+
+  def init_name(raw_path: Path): Document.Node.Name =
   {
     val path = raw_path.expand
     val node = path.implode
-    val qualifier = if (global) "" else session_name
-    val theory = Long_Name.qualify(qualifier, Thy_Header.thy_name(node).getOrElse(""))
+    val theory = qualify(Thy_Header.thy_name(node).getOrElse(""))
     val master_dir = if (theory == "") "" else path.dir.implode
     Document.Node.Name(node, master_dir, theory)
   }
diff -r ce09e947c1d5 -r b722ee40c26c src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Tue Apr 04 18:43:58 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Tue Apr 04 19:40:47 2017 +0200
@@ -30,6 +30,7 @@
   }
 
   sealed case class Base(
+    global_theories: Set[String] = Set.empty,
     loaded_theories: Set[String] = Set.empty,
     known_theories: Map[String, Document.Node.Name] = Map.empty,
     keywords: Thy_Header.Keywords = Nil,
@@ -54,7 +55,9 @@
       verbose: Boolean = false,
       list_files: Boolean = false,
       check_keywords: Set[String] = Set.empty,
+      global_theories: Set[String] = Set.empty,
       tree: Tree): Deps =
+  {
     Deps((Map.empty[String, Base] /: tree.topological_order)(
       { case (deps, (name, info)) =>
           if (progress.stopped) throw Exn.Interrupt()
@@ -78,9 +81,9 @@
             {
               val root_theories =
                 info.theories.flatMap({
-                  case (global, _, thys) =>
+                  case (_, _, thys) =>
                     thys.map(thy =>
-                      (resources.init_name(global, info.dir + resources.thy_path(thy)), info.pos))
+                      (resources.init_name(info.dir + resources.thy_path(thy)), info.pos))
                 })
               val thy_deps = resources.thy_info.dependencies(root_theories)
 
@@ -132,14 +135,17 @@
             if (check_keywords.nonEmpty)
               Check_Keywords.check_keywords(progress, syntax.keywords, check_keywords, theory_files)
 
-            val sources = all_files.map(p => (p, SHA1.digest(p.file)))
+            val base =
+              Base(global_theories = global_theories,
+                loaded_theories = loaded_theories,
+                known_theories = known_theories,
+                keywords = keywords,
+                syntax = syntax,
+                sources = all_files.map(p => (p, SHA1.digest(p.file))),
+                session_graph =
+                  Present.session_graph(info.parent getOrElse "",
+                    parent_base.loaded_theories, thy_deps.deps))
 
-            val session_graph =
-              Present.session_graph(info.parent getOrElse "",
-                parent_base.loaded_theories, thy_deps.deps)
-
-            val base =
-              Base(loaded_theories, known_theories, keywords, syntax, sources, session_graph)
             deps + (name -> base)
           }
           catch {
@@ -148,11 +154,14 @@
                 quote(name) + Position.here(info.pos))
           }
       }))
+  }
 
   def session_base(options: Options, session: String, dirs: List[Path] = Nil): Base =
   {
-    val (_, tree) = load(options, dirs = dirs).selection(sessions = List(session))
-    dependencies(tree = tree)(session)
+    val full_tree = load(options, dirs = dirs)
+    val (_, tree) = full_tree.selection(sessions = List(session))
+
+    dependencies(global_theories = full_tree.global_theories, tree = tree)(session)
   }
 
 
@@ -173,6 +182,10 @@
     meta_digest: SHA1.Digest)
   {
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
+
+    def global_theories: List[String] =
+      for { (global, _, paths) <- theories if global; path <- paths }
+      yield path.base.implode
   }
 
   object Tree
@@ -207,6 +220,7 @@
                 }
             }
         }
+
       new Tree(graph2)
     }
   }
@@ -217,6 +231,12 @@
     def apply(name: String): Info = graph.get_node(name)
     def isDefinedAt(name: String): Boolean = graph.defined(name)
 
+    def global_theories: Set[String] =
+      (for {
+        (_, (info, _)) <- graph.iterator
+        name <- info.global_theories.iterator }
+       yield name).toSet
+
     def selection(
       requirements: Boolean = false,
       all_sessions: Boolean = false,
diff -r ce09e947c1d5 -r b722ee40c26c src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Apr 04 18:43:58 2017 +0200
+++ b/src/Pure/Tools/build.scala	Tue Apr 04 19:40:47 2017 +0200
@@ -396,7 +396,9 @@
     val full_tree = Sessions.load(build_options, dirs, select_dirs)
     val (selected, selected_tree) = selection(full_tree)
     val deps =
-      Sessions.dependencies(progress, true, verbose, list_files, check_keywords, selected_tree)
+      Sessions.dependencies(
+        progress, true, verbose, list_files, check_keywords,
+          full_tree.global_theories, selected_tree)
 
     def sources_stamp(name: String): List[String] =
       (selected_tree(name).meta_digest :: deps.sources(name)).map(_.toString).sorted