# HG changeset patch
# User wenzelm
# Date 1605652001 -3600
# Node ID fffad9ad660efac8de637c5ae327277f1989126e
# Parent  db5f4572704a8681d5438f2f9bd80f33455a0d6d
simplified/clarified persistent session information;

diff -r db5f4572704a -r fffad9ad660e src/Pure/PIDE/session.ML
--- a/src/Pure/PIDE/session.ML	Tue Nov 17 22:58:55 2020 +0100
+++ b/src/Pure/PIDE/session.ML	Tue Nov 17 23:26:41 2020 +0100
@@ -6,10 +6,10 @@
 
 signature SESSION =
 sig
+  val init: string -> unit
   val get_name: unit -> string
   val welcome: unit -> string
   val get_keywords: unit -> Keyword.keywords
-  val init: string -> string * string -> unit
   val shutdown: unit -> unit
   val finish: unit -> unit
 end;
@@ -17,11 +17,13 @@
 structure Session: SESSION =
 struct
 
-(** persistent session information **)
+(* session name *)
+
+val session = Synchronized.var "Session.session" "";
 
-val session = Synchronized.var "Session.session" ({chapter = "", name = ""}, true);
+fun init name = Synchronized.change session (K name);
 
-fun get_name () = #name (#1 (Synchronized.value session));
+fun get_name () = Synchronized.value session;
 
 fun description () = "Isabelle/" ^ get_name ();
 
@@ -43,15 +45,6 @@
       (Thy_Info.get_names ()) Keyword.empty_keywords));
 
 
-(* init *)
-
-fun init parent (chapter, name) =
-  (Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) =>
-    if parent_name <> parent orelse not parent_finished then
-      error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
-    else ({chapter = chapter, name = name}, false)));
-
-
 (* finish *)
 
 fun shutdown () =
@@ -64,7 +57,6 @@
   Par_List.map (Global_Theory.get_thm_names o Thy_Info.get_theory) (Thy_Info.get_names ());
   Thy_Info.finish ();
   shutdown ();
-  update_keywords ();
-  Synchronized.change session (apsnd (K true)));
+  update_keywords ());
 
 end;
diff -r db5f4572704a -r fffad9ad660e src/Pure/Tools/build.ML
--- a/src/Pure/Tools/build.ML	Tue Nov 17 22:58:55 2020 +0100
+++ b/src/Pure/Tools/build.ML	Tue Nov 17 23:26:41 2020 +0100
@@ -54,20 +54,17 @@
     (fn [resources_yxml, args_yxml] =>
         let
           val _ = Resources.init_session_yxml resources_yxml;
-          val (parent_name, (chapter, (session_name, theories))) =
+          val (session_name, theories) =
             YXML.parse_body args_yxml |>
               let
                 open XML.Decode;
                 val position = Position.of_properties o properties;
-              in
-                pair string (pair string (pair string
-                  (list (pair Options.decode (list (pair string position))))))
-              end;
+              in pair string (list (pair Options.decode (list (pair string position)))) end;
+
+          val _ = Session.init session_name;
 
           fun build () =
             let
-              val _ = Session.init parent_name (chapter, session_name);
-
               val res1 =
                 theories |>
                   (List.app (build_theories session_name)
diff -r db5f4572704a -r fffad9ad660e src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Nov 17 22:58:55 2020 +0100
+++ b/src/Pure/Tools/build.scala	Tue Nov 17 23:26:41 2020 +0100
@@ -341,9 +341,8 @@
                   YXML.string_of_body(
                     {
                       import XML.Encode._
-                      pair(string, pair(string, pair(string,
-                        list(pair(Options.encode, list(pair(string, properties)))))))(
-                        (parent, (info.chapter, (session_name, info.theories))))
+                      pair(string, list(pair(Options.encode, list(pair(string, properties)))))(
+                        (session_name, info.theories))
                     })
                 session.protocol_command("build_session", resources_yxml, args_yxml)
                 Build_Session_Errors.result