isabelle: src/Pure/PIDE/session.ML@f458547b4f0f (annotated)

56210 c7c85cdb725d clarified module arrangement; wenzelm parents: 55386 diff changeset	1	(* Title: Pure/PIDE/session.ML
52052 892061142ba6 discontinued obsolete isabelle usedir, mkdir, make; wenzelm parents: 52050 diff changeset	2	Author: Makarius
6346 643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	3
56210 c7c85cdb725d clarified module arrangement; wenzelm parents: 55386 diff changeset	4	Prover session: persistent state of logic image.
6346 643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	5	*)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	6
643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	7	signature SESSION =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	8	sig
72640 fffad9ad660e simplified/clarified persistent session information; wenzelm parents: 72622 diff changeset	9	val init: string -> unit
60081 9fb7b44e3e7e tuned signature; wenzelm parents: 59448 diff changeset	10	val get_name: unit -> string
6346 643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	11	val welcome: unit -> string
59369 7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message; wenzelm parents: 59345 diff changeset	12	val shutdown: unit -> unit
48457 fd9e28d5a143 pass build options to ML; wenzelm parents: 48445 diff changeset	13	val finish: unit -> unit
6346 643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	14	end;
643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	15
643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	16	structure Session: SESSION =
643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	17	struct
643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	18
72640 fffad9ad660e simplified/clarified persistent session information; wenzelm parents: 72622 diff changeset	19	(* session name *)
fffad9ad660e simplified/clarified persistent session information; wenzelm parents: 72622 diff changeset	20
fffad9ad660e simplified/clarified persistent session information; wenzelm parents: 72622 diff changeset	21	val session = Synchronized.var "Session.session" "";
6346 643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	22
72640 fffad9ad660e simplified/clarified persistent session information; wenzelm parents: 72622 diff changeset	23	fun init name = Synchronized.change session (K name);
48542 0a5f598cacec simplified Session.name; wenzelm parents: 48518 diff changeset	24
72640 fffad9ad660e simplified/clarified persistent session information; wenzelm parents: 72622 diff changeset	25	fun get_name () = Synchronized.value session;
60081 9fb7b44e3e7e tuned signature; wenzelm parents: 59448 diff changeset	26
73776 9f205ca4178a tuned message, e.g. for Pure bootstrap; wenzelm parents: 73523 diff changeset	27	fun description () = (case get_name () of "" => "Isabelle" \| name => "Isabelle/" ^ name);
30173 eabece26b89b moved isabelle_process.ML, isabelle_process.scala, isar.ML, session.ML to Pure/System/ (together with associated Isar commands); wenzelm parents: 29435 diff changeset	28
73523 2cd23d587db9 further clarification of Isabelle distribution identification -- avoid odd patching of sources; wenzelm parents: 72640 diff changeset	29	fun welcome () = "Welcome to " ^ description () ^ Isabelle_System.isabelle_heading ();
6346 643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	30
643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	31
643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	32	(* finish *)
643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	33
59369 7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message; wenzelm parents: 59345 diff changeset	34	fun shutdown () =
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message; wenzelm parents: 59345 diff changeset	35	(Execution.shutdown ();
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message; wenzelm parents: 59345 diff changeset	36	Event_Timer.shutdown ();
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message; wenzelm parents: 59345 diff changeset	37	Future.shutdown ());
7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message; wenzelm parents: 59345 diff changeset	38
6346 643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	39	fun finish () =
59369 7090199d3f78 more informative build_theories_result: cumulative Runtime.exn_message; wenzelm parents: 59345 diff changeset	40	(shutdown ();
72098 8c547eac8381 more robust treatment of thm_names, with strict check after all theories are loaded; wenzelm parents: 71611 diff changeset	41	Par_List.map (Global_Theory.get_thm_names o Thy_Info.get_theory) (Thy_Info.get_names ());
49911 262c36fd5f26 collective errors from use_thys and Session.finish/Goal.finish_futures -- avoid uninformative interrupts stemming from failure of goal forks that are not registered in the theory (e.g. unnamed theorems); wenzelm parents: 49895 diff changeset	42	Thy_Info.finish ();
76406 40a365360680 more accurate outer syntax keywords (see also 94b2690ad494): base session could be anything, e.g. ZF vs. HOL; wenzelm parents: 73776 diff changeset	43	shutdown ());
6346 643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	44
643a1bd31a91 moved Thy/session.ML to Isar/session.ML; wenzelm parents: diff changeset	45	end;

author	wenzelm
	Mon, 13 Mar 2023 11:02:26 +0100
changeset 77622	f458547b4f0f
parent 76406	40a365360680
child 78020	1a829342a2d3
permissions	-rw-r--r--