| author | wenzelm |
| Fri, 08 Jan 2021 16:36:20 +0100 | |
| changeset 73105 | 578a33042aa6 |
| parent 72640 | fffad9ad660e |
| child 73523 | 2cd23d587db9 |
| 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 |
|
|
72640
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72622
diff
changeset
|
9 |
val init: string -> unit |
| 60081 | 10 |
val get_name: unit -> string |
| 6346 | 11 |
val welcome: unit -> string |
|
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
58928
diff
changeset
|
12 |
val get_keywords: unit -> Keyword.keywords |
|
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 |
||
|
72640
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72622
diff
changeset
|
20 |
(* session name *) |
|
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72622
diff
changeset
|
21 |
|
|
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72622
diff
changeset
|
22 |
val session = Synchronized.var "Session.session" ""; |
| 6346 | 23 |
|
|
72640
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72622
diff
changeset
|
24 |
fun init name = Synchronized.change session (K name); |
| 48542 | 25 |
|
|
72640
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72622
diff
changeset
|
26 |
fun get_name () = Synchronized.value session; |
| 60081 | 27 |
|
28 |
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
|
29 |
|
|
26109
c69c3559355b
more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents:
25840
diff
changeset
|
30 |
fun welcome () = |
|
57649
a43898f76ae9
further distinction of Isabelle distribution: alert for identified release candidates;
wenzelm
parents:
56533
diff
changeset
|
31 |
if Distribution.is_identified then |
| 60081 | 32 |
"Welcome to " ^ description () ^ " (" ^ Distribution.version ^ ")"
|
33 |
else "Unofficial version of " ^ description () ^ " (" ^ Distribution.version ^ ")";
|
|
| 6346 | 34 |
|
35 |
||
|
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
58928
diff
changeset
|
36 |
(* base syntax *) |
|
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
58928
diff
changeset
|
37 |
|
| 62928 | 38 |
val keywords = Synchronized.var "Session.keywords" Keyword.empty_keywords; |
39 |
||
40 |
fun get_keywords () = Synchronized.value keywords; |
|
41 |
||
42 |
fun update_keywords () = |
|
43 |
Synchronized.change keywords |
|
44 |
(K (fold (curry Keyword.merge_keywords o Thy_Header.get_keywords o Thy_Info.get_theory) |
|
45 |
(Thy_Info.get_names ()) Keyword.empty_keywords)); |
|
|
59086
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
58928
diff
changeset
|
46 |
|
|
94b2690ad494
node-specific keywords, with session base syntax as default;
wenzelm
parents:
58928
diff
changeset
|
47 |
|
| 6346 | 48 |
(* finish *) |
49 |
||
|
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
50 |
fun shutdown () = |
|
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
51 |
(Execution.shutdown (); |
|
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
52 |
Event_Timer.shutdown (); |
|
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
53 |
Future.shutdown ()); |
|
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
54 |
|
| 6346 | 55 |
fun finish () = |
|
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
56 |
(shutdown (); |
|
72098
8c547eac8381
more robust treatment of thm_names, with strict check after all theories are loaded;
wenzelm
parents:
71611
diff
changeset
|
57 |
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
|
58 |
Thy_Info.finish (); |
|
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
59 |
shutdown (); |
|
72640
fffad9ad660e
simplified/clarified persistent session information;
wenzelm
parents:
72622
diff
changeset
|
60 |
update_keywords ()); |
| 6346 | 61 |
|
62 |
end; |