src/Pure/PIDE/resources.ML

--- a/src/Pure/PIDE/resources.ML	Thu Sep 28 11:53:55 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Thu Sep 28 15:11:32 2017 +0200
@@ -9,11 +9,11 @@
   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
@@ -39,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 =
@@ -49,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 () =
@@ -62,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;
 
 
@@ -107,15 +107,14 @@
     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