| author | wenzelm |
| Thu, 11 May 2023 12:20:47 +0200 | |
| changeset 78032 | 73c77db63594 |
| parent 78020 | 1a829342a2d3 |
| child 78034 | 37085099e415 |
| 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 |
|
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
12 |
val shutdown: unit -> unit |
| 48457 | 13 |
val finish: unit -> unit |
| 78032 | 14 |
val print_context_tracing: (Context.generic -> bool) -> 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 |
|
| 73776 | 28 |
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
|
29 |
|
|
73523
2cd23d587db9
further clarification of Isabelle distribution identification -- avoid odd patching of sources;
wenzelm
parents:
72640
diff
changeset
|
30 |
fun welcome () = "Welcome to " ^ description () ^ Isabelle_System.isabelle_heading (); |
| 6346 | 31 |
|
32 |
||
33 |
(* finish *) |
|
34 |
||
|
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
35 |
fun shutdown () = |
|
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
36 |
(Execution.shutdown (); |
|
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
37 |
Event_Timer.shutdown (); |
|
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
38 |
Future.shutdown ()); |
|
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
39 |
|
| 6346 | 40 |
fun finish () = |
|
59369
7090199d3f78
more informative build_theories_result: cumulative Runtime.exn_message;
wenzelm
parents:
59345
diff
changeset
|
41 |
(shutdown (); |
|
72098
8c547eac8381
more robust treatment of thm_names, with strict check after all theories are loaded;
wenzelm
parents:
71611
diff
changeset
|
42 |
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
|
43 |
Thy_Info.finish (); |
| 78020 | 44 |
Context.finish_tracing (); |
|
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
|
45 |
shutdown ()); |
| 6346 | 46 |
|
| 78032 | 47 |
fun print_context_tracing pred = |
48 |
List.app (writeln o Proof_Display.print_context_tracing) |
|
49 |
(filter (pred o #1) (#contexts (Context.finish_tracing ()))); |
|
50 |
||
| 6346 | 51 |
end; |