# HG changeset patch
# User wenzelm
# Date 1492079976 -7200
# Node ID 7c40477e0a879dd46355c1dbb4f828793ce19c44
# Parent  64e61b0f6972d7f1094a7f1ec32080ca2dac60f0
clarified init_session_base / finish_session_base: retain some information for plain "isabelle process", without rechecking dependencies as in "isabelle console";

diff -r 64e61b0f6972 -r 7c40477e0a87 src/Pure/ML/ml_process.scala
--- a/src/Pure/ML/ml_process.scala	Thu Apr 13 12:27:57 2017 +0200
+++ b/src/Pure/ML/ml_process.scala	Thu Apr 13 12:39:36 2017 +0200
@@ -99,7 +99,7 @@
             ML_Syntax.print_list(
               ML_Syntax.print_pair(
                 ML_Syntax.print_string, ML_Syntax.print_string))(table)
-          List("Resources.set_session_base {default_qualifier = \"\"" +
+          List("Resources.init_session_base {default_qualifier = \"\"" +
             ", global_theories = " + print_table(base.global_theories.toList) +
             ", loaded_theories = " + print_table(base.loaded_theories.toList) +
             ", known_theories = " + print_table(base.dest_known_theories) + "}")
diff -r 64e61b0f6972 -r 7c40477e0a87 src/Pure/PIDE/protocol.ML
--- a/src/Pure/PIDE/protocol.ML	Thu Apr 13 12:27:57 2017 +0200
+++ b/src/Pure/PIDE/protocol.ML	Thu Apr 13 12:39:36 2017 +0200
@@ -23,7 +23,7 @@
       let
         val decode_table = YXML.parse_body #> let open XML.Decode in list (pair string string) end;
       in
-        Resources.set_session_base
+        Resources.init_session_base
           {default_qualifier = default_qualifier,
            global_theories = decode_table global_theories_yxml,
            loaded_theories = decode_table loaded_theories_yxml,
diff -r 64e61b0f6972 -r 7c40477e0a87 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);
 
diff -r 64e61b0f6972 -r 7c40477e0a87 src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Thu Apr 13 12:27:57 2017 +0200
+++ b/src/Pure/Tools/build.ML	Thu Apr 13 12:39:36 2017 +0200
@@ -180,7 +180,7 @@
     val symbols = HTML.make_symbols symbol_codes;
 
     val _ =
-      Resources.set_session_base
+      Resources.init_session_base
         {default_qualifier = name,
          global_theories = global_theories,
          loaded_theories = loaded_theories,
@@ -210,7 +210,7 @@
           |> Exn.capture);
     val res2 = Exn.capture Session.finish ();
 
-    val _ = Resources.reset_session_base ();
+    val _ = Resources.finish_session_base ();
     val _ = Par_Exn.release_all [res1, res2];
   in () end;