src/Pure/PIDE/resources.ML

--- a/src/Pure/PIDE/resources.ML	Fri Apr 21 13:51:43 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Fri Apr 21 14:09:03 2017 +0200
@@ -6,13 +6,12 @@
 
 signature RESOURCES =
 sig
+  val default_qualifier: string
   val init_session_base:
-    {default_qualifier: string,
-     global_theories: (string * string) list,
+    {global_theories: (string * string) list,
      loaded_theories: (string * string) list,
      known_theories: (string * string) list} -> unit
   val finish_session_base: unit -> unit
-  val default_qualifier: unit -> string
   val global_theory: string -> string option
   val loaded_theory: string -> string option
   val known_theory: string -> Path.T option
@@ -37,36 +36,32 @@
 
 (* session base *)
 
+val default_qualifier = "Draft";
+
 val empty_session_base =
-  {default_qualifier = "Draft",
-   global_theories = Symtab.empty: string Symtab.table,
+  {global_theories = Symtab.empty: string Symtab.table,
    loaded_theories = Symtab.empty: string Symtab.table,
    known_theories = Symtab.empty: Path.T Symtab.table};
 
 val global_session_base =
   Synchronized.var "Sessions.base" empty_session_base;
 
-fun init_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
+fun init_session_base {global_theories, loaded_theories, known_theories} =
   Synchronized.change global_session_base
     (fn _ =>
-      {default_qualifier =
-        if default_qualifier <> "" then default_qualifier
-        else #default_qualifier empty_session_base,
-       global_theories = Symtab.make global_theories,
+      {global_theories = Symtab.make global_theories,
        loaded_theories = Symtab.make loaded_theories,
        known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
 
 fun finish_session_base () =
   Synchronized.change global_session_base
     (fn {global_theories, loaded_theories, ...} =>
-      {default_qualifier = #default_qualifier empty_session_base,
-       global_theories = global_theories,
+      {global_theories = global_theories,
        loaded_theories = loaded_theories,
        known_theories = #known_theories empty_session_base});
 
 fun get_session_base f = f (Synchronized.value global_session_base);
 
-fun default_qualifier () = get_session_base #default_qualifier;
 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;