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 =