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;