# HG changeset patch
# User wenzelm
# Date 1491835392 -7200
# Node ID 2bf0d2fcd506443fa1a2b7acc7973c360bb0bfe1
# Parent  31e8a86971a88bd11ebfd3010e9bd6aae4f25986
proper import qualifier for global theories;
clarified uniqueness;

diff -r 31e8a86971a8 -r 2bf0d2fcd506 src/Pure/PIDE/resources.ML
--- a/src/Pure/PIDE/resources.ML	Mon Apr 10 13:30:55 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Mon Apr 10 16:43:12 2017 +0200
@@ -8,12 +8,12 @@
 sig
   val set_session_base:
     {default_qualifier: string,
-     global_theories: string list,
+     global_theories: (string * string) list,
      loaded_theories: (string * string) list,
      known_theories: (string * string) list} -> unit
   val reset_session_base: unit -> unit
   val default_qualifier: unit -> string
-  val global_theory: string -> bool
+  val global_theory: string -> string option
   val loaded_theory: string -> Path.T option
   val known_theory: string -> Path.T option
   val master_directory: theory -> Path.T
@@ -42,7 +42,7 @@
 
 val init_session_base =
   {default_qualifier = "Draft",
-   global_theories = Symtab.make_set [],
+   global_theories = Symtab.empty: string Symtab.table,
    loaded_theories = Symtab.empty: Path.T Symtab.table,
    known_theories = Symtab.empty: Path.T Symtab.table};
 
@@ -55,7 +55,7 @@
       {default_qualifier =
         if default_qualifier <> "" then default_qualifier
         else #default_qualifier init_session_base,
-       global_theories = Symtab.make_set global_theories,
+       global_theories = Symtab.make global_theories,
        loaded_theories = Symtab.make (map (apsnd Path.explode) loaded_theories),
        known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
 
@@ -65,7 +65,7 @@
 fun get_session_base f = f (Synchronized.value global_session_base);
 
 fun default_qualifier () = get_session_base #default_qualifier;
-fun global_theory a = Symtab.defined (get_session_base #global_theories) a;
+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 known_theory a = Symtab.lookup (get_session_base #known_theories) a;
 
@@ -104,13 +104,15 @@
 val thy_path = Path.ext "thy";
 
 fun theory_qualifier theory =
-  Long_Name.qualifier theory;
+  (case global_theory theory of
+    SOME qualifier => qualifier
+  | NONE => Long_Name.qualifier theory);
 
 fun import_name qualifier dir s =
   let
     val theory0 = Thy_Header.import_name s;
     val theory =
-      if Long_Name.is_qualified theory0 orelse global_theory theory0
+      if Long_Name.is_qualified theory0 orelse is_some (global_theory theory0)
         orelse true (* FIXME *) then theory0
       else Long_Name.qualify qualifier theory0;
     val node_name =
diff -r 31e8a86971a8 -r 2bf0d2fcd506 src/Pure/PIDE/resources.scala
--- a/src/Pure/PIDE/resources.scala	Mon Apr 10 13:30:55 2017 +0200
+++ b/src/Pure/PIDE/resources.scala	Mon Apr 10 16:43:12 2017 +0200
@@ -68,13 +68,13 @@
     else Nil
 
   def theory_qualifier(name: Document.Node.Name): String =
-    Long_Name.qualifier(name.theory)
+    session_base.global_theories.getOrElse(name.theory, Long_Name.qualifier(name.theory))
 
   def import_name(qualifier: String, dir: String, s: String): Document.Node.Name =
   {
     val theory0 = Thy_Header.import_name(s)
     val theory =
-      if (Long_Name.is_qualified(theory0) || session_base.global_theories.contains(theory0)
+      if (Long_Name.is_qualified(theory0) || session_base.global_theories.isDefinedAt(theory0)
         || true /* FIXME */) theory0
       else theory0 // FIXME Long_Name.qualify(qualifier, theory0)
 
diff -r 31e8a86971a8 -r 2bf0d2fcd506 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Apr 10 13:30:55 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Apr 10 16:43:12 2017 +0200
@@ -49,7 +49,7 @@
   }
 
   sealed case class Base(
-    global_theories: Set[String] = Set.empty,
+    global_theories: Map[String, String] = Map.empty,
     loaded_theories: Map[String, Document.Node.Name] = Map.empty,
     known_theories: Map[String, Document.Node.Name] = Map.empty,
     keywords: Thy_Header.Keywords = Nil,
@@ -85,7 +85,7 @@
       verbose: Boolean = false,
       list_files: Boolean = false,
       check_keywords: Set[String] = Set.empty,
-      global_theories: Set[String] = Set.empty): Deps =
+      global_theories: Map[String, String] = Map.empty): Deps =
   {
     Deps((Map.empty[String, Base] /: sessions.imports_topological_order)({
       case (sessions, (session_name, info)) =>
@@ -98,7 +98,7 @@
               case Some(parent) => sessions(parent)
             }
           val resources = new Resources(parent_base,
-            default_qualifier = info.theory_qualifier getOrElse session_name)
+            default_qualifier = info.theory_qualifier(session_name))
 
           if (verbose || list_files) {
             val groups =
@@ -211,10 +211,10 @@
   {
     def timeout: Time = Time.seconds(options.real("timeout") * options.real("timeout_scale"))
 
-    def theory_qualifier: Option[String] =
+    def theory_qualifier(default_qualifier: String): String =
       options.string("theory_qualifier") match {
-        case "" => None
-        case qualifier => Some(qualifier)
+        case "" => default_qualifier
+        case qualifier => qualifier
       }
   }
 
@@ -324,17 +324,19 @@
     def get(name: String): Option[Info] =
       if (imports_graph.defined(name)) Some(imports_graph.get_node(name)) else None
 
-    def global_theories: Set[String] =
-      (Set.empty[String] /:
+    def global_theories: Map[String, String] =
+      (Map.empty[String, String] /:
         (for {
-          (_, (info, _)) <- imports_graph.iterator
-          thy <- info.global_theories.iterator }
-         yield (thy, info.pos)))(
-          { case (set, (thy, pos)) =>
-             if (set.contains(thy))
-               error("Duplicate declaration of global theory " + quote(thy) + Position.here(pos))
-             else set + thy
-           })
+          (session_name, (info, _)) <- imports_graph.iterator
+          thy <- info.global_theories.iterator } yield (thy, session_name, info)))({
+            case (global, (thy, session_name, info)) =>
+              val qualifier = info.theory_qualifier(session_name)
+              global.get(thy) match {
+                case Some(qualifier1) if qualifier != qualifier1 =>
+                  error("Duplicate global theory " + quote(thy) + Position.here(info.pos))
+                case _ => global + (thy -> qualifier)
+              }
+          })
 
     def selection(select: Selection): (List[String], T) =
     {
diff -r 31e8a86971a8 -r 2bf0d2fcd506 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Mon Apr 10 13:30:55 2017 +0200
+++ b/src/Pure/Tools/build.ML	Mon Apr 10 16:43:12 2017 +0200
@@ -146,7 +146,7 @@
   name: string,
   master_dir: Path.T,
   theories: (Options.T * (string * Position.T) list) list,
-  global_theories: string list,
+  global_theories: (string * string) list,
   loaded_theories: (string * string) list,
   known_theories: (string * string) list};
 
@@ -160,7 +160,7 @@
         (pair (list (pair string string)) (pair string (pair string (pair string (pair string
           (pair string
             (pair (((list (pair Options.decode (list (string #> rpair Position.none))))))
-              (pair (list string)
+              (pair (list (pair string string))
                 (pair (list (pair string string)) (list (pair string string)))))))))))))))
       (YXML.parse_body yxml);
   in
diff -r 31e8a86971a8 -r 2bf0d2fcd506 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Mon Apr 10 13:30:55 2017 +0200
+++ b/src/Pure/Tools/build.scala	Mon Apr 10 16:43:12 2017 +0200
@@ -205,7 +205,7 @@
                 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(string))),
-                pair(list(string),
+                pair(list(pair(string, string)),
                 pair(list(pair(string, string)), list(pair(string, string))))))))))))))))(
               (Symbol.codes, (command_timings, (do_output, (verbose,
                 (store.browser_info, (info.document_files, (File.standard_path(graph_file),
@@ -224,8 +224,8 @@
             ML_Syntax.print_string0(File.platform_path(output))
 
         if (pide && !Sessions.is_pure(name)) {
-          val resources = new Resources(deps(parent),
-            default_qualifier = info.theory_qualifier getOrElse name)
+          val resources =
+            new Resources(deps(parent), default_qualifier = info.theory_qualifier(name))
           val session = new Session(options, resources)
           val handler = new Handler(progress, session, name)
           session.init_protocol_handler(handler)
diff -r 31e8a86971a8 -r 2bf0d2fcd506 src/Pure/Tools/ml_process.scala
--- a/src/Pure/Tools/ml_process.scala	Mon Apr 10 13:30:55 2017 +0200
+++ b/src/Pure/Tools/ml_process.scala	Mon Apr 10 16:43:12 2017 +0200
@@ -100,8 +100,7 @@
               ML_Syntax.print_pair(
                 ML_Syntax.print_string, ML_Syntax.print_string))(table)
           List("Resources.set_session_base {default_qualifier = \"\"" +
-            ", global_theories = " +
-              ML_Syntax.print_list(ML_Syntax.print_string)(base.global_theories.toList) +
+            ", global_theories = " + print_table(base.global_theories.toList) +
             ", loaded_theories = " + print_table(base.dest_loaded_theories) +
             ", known_theories = " + print_table(base.dest_known_theories) + "}")
       }