author | wenzelm |
Wed, 11 Nov 2020 21:00:14 +0100 | |
changeset 72574 | d892f6d66402 |
parent 72309 | 564012e31db1 |
child 72620 | 429afd0d1a79 |
permissions | -rw-r--r-- |
56210 | 1 |
(* Title: Pure/PIDE/session.ML |
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52050
diff
changeset
|
2 |
Author: Makarius |
6346 | 3 |
|
56210 | 4 |
Prover session: persistent state of logic image. |
6346 | 5 |
*) |
6 |
||
7 |
signature SESSION = |
|
8 |
sig |
|
60081 | 9 |
val get_name: unit -> string |
6346 | 10 |
val welcome: unit -> string |
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
58928
diff
changeset
|
11 |
val get_keywords: unit -> Keyword.keywords |
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
12 |
val init: HTML.symbols -> bool -> Path.T -> string list -> string -> string * string -> bool -> unit |
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
13 |
val shutdown: unit -> unit |
48457 | 14 |
val finish: unit -> unit |
6346 | 15 |
end; |
16 |
||
17 |
structure Session: SESSION = |
|
18 |
struct |
|
19 |
||
62928 | 20 |
(** persistent session information **) |
6346 | 21 |
|
62944
3ee643c5ed00
more standard session build process, including browser_info;
wenzelm
parents:
62936
diff
changeset
|
22 |
val session = Synchronized.var "Session.session" ({chapter = "", name = ""}, true); |
48542 | 23 |
|
62928 | 24 |
fun get_name () = #name (#1 (Synchronized.value session)); |
60081 | 25 |
|
26 |
fun description () = "Isabelle/" ^ get_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
|
27 |
|
26109
c69c3559355b
more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents:
25840
diff
changeset
|
28 |
fun welcome () = |
57649
a43898f76ae9
further distinction of Isabelle distribution: alert for identified release candidates;
wenzelm
parents:
56533
diff
changeset
|
29 |
if Distribution.is_identified then |
60081 | 30 |
"Welcome to " ^ description () ^ " (" ^ Distribution.version ^ ")" |
31 |
else "Unofficial version of " ^ description () ^ " (" ^ Distribution.version ^ ")"; |
|
6346 | 32 |
|
33 |
||
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
58928
diff
changeset
|
34 |
(* base syntax *) |
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
58928
diff
changeset
|
35 |
|
62928 | 36 |
val keywords = Synchronized.var "Session.keywords" Keyword.empty_keywords; |
37 |
||
38 |
fun get_keywords () = Synchronized.value keywords; |
|
39 |
||
40 |
fun update_keywords () = |
|
41 |
Synchronized.change keywords |
|
42 |
(K (fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory) |
|
43 |
(Thy_Info.get_names ()) Keyword.empty_keywords)); |
|
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
58928
diff
changeset
|
44 |
|
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
58928
diff
changeset
|
45 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
46 |
(* init *) |
9414 | 47 |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
48 |
fun init symbols info info_path documents parent (chapter, name) verbose = |
62928 | 49 |
(Synchronized.change session (fn ({name = parent_name, ...}, parent_finished) => |
50 |
if parent_name <> parent orelse not parent_finished then |
|
51 |
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) |
|
52 |
else ({chapter = chapter, name = name}, false)); |
|
72574
d892f6d66402
build documents in Isabelle/Scala, based on generated tex files as session exports;
wenzelm
parents:
72309
diff
changeset
|
53 |
Present.init symbols info info_path documents (chapter, name) verbose); |
6346 | 54 |
|
55 |
||
56 |
(* finish *) |
|
57 |
||
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
58 |
fun shutdown () = |
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
59 |
(Execution.shutdown (); |
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
60 |
Event_Timer.shutdown (); |
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
61 |
Future.shutdown ()); |
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
62 |
|
6346 | 63 |
fun finish () = |
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
64 |
(shutdown (); |
72098
8c547eac8381
more robust treatment of thm_names, with strict check after all theories are loaded;
wenzelm
parents:
71611
diff
changeset
|
65 |
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
|
66 |
Thy_Info.finish (); |
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
|
67 |
Present.finish (); |
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
68 |
shutdown (); |
62928 | 69 |
update_keywords (); |
70 |
Synchronized.change session (apsnd (K true))); |
|
6346 | 71 |
|
72 |
end; |