src/Pure/PIDE/resources.ML

--- a/src/Pure/PIDE/resources.ML	Thu Apr 13 12:27:57 2017 +0200
+++ b/src/Pure/PIDE/resources.ML	Thu Apr 13 12:39:36 2017 +0200
@@ -6,12 +6,12 @@
 
 signature RESOURCES =
 sig
-  val set_session_base:
+  val init_session_base:
     {default_qualifier: string,
      global_theories: (string * string) list,
      loaded_theories: (string * string) list,
      known_theories: (string * string) list} -> unit
-  val reset_session_base: unit -> unit
+  val finish_session_base: unit -> unit
   val default_qualifier: unit -> string
   val global_theory: string -> string option
   val loaded_theory: string -> string option
@@ -40,27 +40,32 @@
 
 (* session base *)
 
-val init_session_base =
+val empty_session_base =
   {default_qualifier = "Draft",
    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" init_session_base;
+  Synchronized.var "Sessions.base" empty_session_base;
 
-fun set_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
+fun init_session_base {default_qualifier, global_theories, loaded_theories, known_theories} =
   Synchronized.change global_session_base
     (fn _ =>
       {default_qualifier =
         if default_qualifier <> "" then default_qualifier
-        else #default_qualifier init_session_base,
+        else #default_qualifier empty_session_base,
        global_theories = Symtab.make global_theories,
        loaded_theories = Symtab.make loaded_theories,
        known_theories = Symtab.make (map (apsnd Path.explode) known_theories)});
 
-fun reset_session_base () =
-  Synchronized.change global_session_base (K init_session_base);
+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,
+       loaded_theories = loaded_theories,
+       known_theories = #known_theories empty_session_base});
 
 fun get_session_base f = f (Synchronized.value global_session_base);