author | wenzelm |
Mon, 20 May 2013 13:38:48 +0200 | |
changeset 52080 | 02749038168b |
parent 52052 | 892061142ba6 |
child 52083 | f852d08376f9 |
permissions | -rw-r--r-- |
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
|
1 |
(* Title: Pure/System/session.ML |
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52050
diff
changeset
|
2 |
Author: Makarius |
6346 | 3 |
|
52052
892061142ba6
discontinued obsolete isabelle usedir, mkdir, make;
wenzelm
parents:
52050
diff
changeset
|
4 |
Session management -- internal state of logic images (not thread-safe). |
6346 | 5 |
*) |
6 |
||
7 |
signature SESSION = |
|
8 |
sig |
|
11509 | 9 |
val name: unit -> string |
6346 | 10 |
val welcome: unit -> string |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
11 |
val init: bool -> bool -> Path.T -> string -> bool -> string -> (string * string) list -> |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
12 |
string -> string * string -> bool * string -> bool -> unit |
48457 | 13 |
val finish: unit -> unit |
6346 | 14 |
end; |
15 |
||
16 |
structure Session: SESSION = |
|
17 |
struct |
|
18 |
||
19 |
(* session state *) |
|
20 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
21 |
val session = Unsynchronized.ref {chapter = "Pure", name = "Pure"}; |
32738 | 22 |
val session_finished = Unsynchronized.ref false; |
48542 | 23 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
24 |
fun name () = "Isabelle/" ^ #name (! session); |
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
|
25 |
|
26109
c69c3559355b
more elaborate structure Distribution (filled-in by makedist);
wenzelm
parents:
25840
diff
changeset
|
26 |
fun welcome () = |
26134 | 27 |
if Distribution.is_official then |
28 |
"Welcome to " ^ name () ^ " (" ^ Distribution.version ^ ")" |
|
48990 | 29 |
else "Unofficial version of " ^ name () ^ " (" ^ Distribution.version ^ ")"; |
6346 | 30 |
|
31 |
||
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
32 |
(* init *) |
9414 | 33 |
|
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
34 |
fun init build info info_path doc doc_graph doc_output doc_variants |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
35 |
parent (chapter, name) doc_dump verbose = |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
36 |
if #name (! session) <> parent orelse not (! session_finished) then |
6346 | 37 |
error ("Unfinished parent session " ^ quote parent ^ " for " ^ quote name) |
51399
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
38 |
else |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
39 |
let |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
40 |
val _ = session := {chapter = chapter, name = name}; |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
41 |
val _ = session_finished := false; |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
42 |
in |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
43 |
Present.init build info info_path (if doc = "false" then "" else doc) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
44 |
doc_graph doc_output doc_variants (chapter, name) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
45 |
doc_dump verbose (map Thy_Info.get_theory (Thy_Info.get_names ())) |
6ac3c29a300e
discontinued "isabelle usedir" option -r (reset session path);
wenzelm
parents:
51398
diff
changeset
|
46 |
end; |
6346 | 47 |
|
48 |
||
49 |
(* finish *) |
|
50 |
||
51 |
fun finish () = |
|
51276 | 52 |
(Goal.shutdown_futures (); |
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
|
53 |
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
|
54 |
Present.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
|
55 |
Keyword.status (); |
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
|
56 |
Outer_Syntax.check_syntax (); |
50430
702278df3b57
make double-sure that the future scheduler is properly shutdown, otherwise its threads are made persistent and will deadlock with the fresh instance after reloading the image (NB: Present.finish involves another Par_List.map over document_variants and thus might fork again);
wenzelm
parents:
50121
diff
changeset
|
57 |
Future.shutdown (); |
52050 | 58 |
Event_Timer.shutdown (); |
52080
02749038168b
reset options last -- other parts of the system may still need them;
wenzelm
parents:
52052
diff
changeset
|
59 |
Options.reset_default (); |
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
|
60 |
session_finished := true); |
6346 | 61 |
|
62 |
end; |