--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/PIDE/session.ML Tue Mar 18 18:09:31 2014 +0100
@@ -0,0 +1,80 @@
+(* Title: Pure/PIDE/session.ML
+ Author: Makarius
+
+Prover session: persistent state of logic image.
+*)
+
+signature SESSION =
+sig
+ val name: unit -> string
+ val welcome: unit -> string
+ val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list ->
+ string -> string * string -> bool * string -> bool -> unit
+ val finish: unit -> unit
+ val protocol_handler: string -> unit
+ val init_protocol_handlers: unit -> unit
+end;
+
+structure Session: SESSION =
+struct
+
+(** session identification -- not thread-safe **)
+
+val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"};
+val session_finished = Unsynchronized.ref false;
+
+fun name () = "Isabelle/" ^ #name (! session);
+
+fun welcome () =
+ if Distribution.is_official then
+ "Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")"
+ else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")";
+
+
+(* init *)
+
+fun init build info info_path doc doc_graph doc_output doc_variants
+ parent (chapter, name) doc_dump verbose =
+ if #name (! session) <> parent orelse not (! session_finished) then
+ error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name)
+ else
+ let
+ val _ = session := {chapter = chapter, name = name};
+ val _ = session_finished := false;
+ in
+ Present.init build info info_path (if doc = "false" then "" else doc)
+ doc_graph doc_output doc_variants (chapter, name)
+ doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ()))
+ end;
+
+
+(* finish *)
+
+fun finish () =
+ (Execution.shutdown ();
+ Thy_Info.finish ();
+ Present.finish ();
+ Outer_Syntax.check_syntax ();
+ Future.shutdown ();
+ Event_Timer.shutdown ();
+ Future.shutdown ();
+ session_finished := true);
+
+
+
+(** protocol handlers **)
+
+val protocol_handlers = Synchronized.var "protocol_handlers" ([]: string list);
+
+fun protocol_handler name =
+ Synchronized.change protocol_handlers (fn handlers =>
+ (Output.try_protocol_message (Markup.protocol_handler name) "";
+ if not (member (op =) handlers name) then ()
+ else warning ("Redefining protocol handler: " ^ quote name);
+ update (op =) name handlers));
+
+fun init_protocol_handlers () =
+ Synchronized.value protocol_handlers
+ |> List.app (fn name => Output.try_protocol_message (Markup.protocol_handler name) "");
+
+end;