author | wenzelm |
Fri, 29 Mar 2013 22:14:27 +0100 | |
changeset 51580 | 64ef8260dc60 |
parent 51560 | 5b4ae2467830 |
child 51595 | 8e9746e584c9 |
permissions | -rw-r--r-- |
5828 | 1 |
(* Title: Pure/Isar/toplevel.ML |
2 |
Author: Markus Wenzel, TU Muenchen |
|
3 |
||
26602
5534b6a6b810
made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset
|
4 |
Isabelle/Isar toplevel transactions. |
5828 | 5 |
*) |
6 |
||
7 |
signature TOPLEVEL = |
|
8 |
sig |
|
19063 | 9 |
exception UNDEF |
5828 | 10 |
type state |
26602
5534b6a6b810
made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset
|
11 |
val toplevel: state |
7732 | 12 |
val is_toplevel: state -> bool |
18589 | 13 |
val is_theory: state -> bool |
14 |
val is_proof: state -> bool |
|
51555 | 15 |
val is_skipped_proof: state -> bool |
17076 | 16 |
val level: state -> int |
30398 | 17 |
val presentation_context_of: state -> Proof.context |
30801 | 18 |
val previous_context_of: state -> Proof.context option |
21506 | 19 |
val context_of: state -> Proof.context |
22089 | 20 |
val generic_theory_of: state -> generic_theory |
5828 | 21 |
val theory_of: state -> theory |
22 |
val proof_of: state -> Proof.state |
|
18589 | 23 |
val proof_position_of: state -> int |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
24 |
val end_theory: Position.T -> state -> theory |
16815 | 25 |
val print_state_context: state -> unit |
26 |
val print_state: bool -> state -> unit |
|
37858 | 27 |
val pretty_abstract: state -> Pretty.T |
32738 | 28 |
val quiet: bool Unsynchronized.ref |
29 |
val debug: bool Unsynchronized.ref |
|
30 |
val interact: bool Unsynchronized.ref |
|
31 |
val timing: bool Unsynchronized.ref |
|
32 |
val profiling: int Unsynchronized.ref |
|
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset
|
33 |
val program: (unit -> 'a) -> 'a |
33604
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
34 |
val thread: bool -> (unit -> unit) -> Thread.thread |
16682 | 35 |
type transition |
5828 | 36 |
val empty: transition |
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset
|
37 |
val print_of: transition -> bool |
27427 | 38 |
val name_of: transition -> string |
28105 | 39 |
val pos_of: transition -> Position.T |
5828 | 40 |
val name: string -> transition -> transition |
41 |
val position: Position.T -> transition -> transition |
|
42 |
val interactive: bool -> transition -> transition |
|
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset
|
43 |
val set_print: bool -> transition -> transition |
5828 | 44 |
val print: transition -> transition |
9010 | 45 |
val no_timing: transition -> transition |
44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset
|
46 |
val init_theory: (unit -> theory) -> transition -> transition |
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset
|
47 |
val is_init: transition -> bool |
44186
806f0ec1a43d
simplified Toplevel.init_theory: discontinued special master argument;
wenzelm
parents:
44185
diff
changeset
|
48 |
val modify_init: (unit -> theory) -> transition -> transition |
6689 | 49 |
val exit: transition -> transition |
5828 | 50 |
val keep: (state -> unit) -> transition -> transition |
7612 | 51 |
val keep': (bool -> state -> unit) -> transition -> transition |
5828 | 52 |
val imperative: (unit -> unit) -> transition -> transition |
27840 | 53 |
val ignored: Position.T -> transition |
51268
fcc4b89a600d
simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
wenzelm
parents:
51241
diff
changeset
|
54 |
val is_ignored: transition -> bool |
27840 | 55 |
val malformed: Position.T -> string -> transition |
48772 | 56 |
val is_malformed: transition -> bool |
26491 | 57 |
val generic_theory: (generic_theory -> generic_theory) -> transition -> transition |
7612 | 58 |
val theory': (bool -> theory -> theory) -> transition -> transition |
49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset
|
59 |
val theory: (theory -> theory) -> transition -> transition |
20985 | 60 |
val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition |
21007 | 61 |
val end_local_theory: transition -> transition |
47069 | 62 |
val open_target: (generic_theory -> local_theory) -> transition -> transition |
63 |
val close_target: transition -> transition |
|
45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset
|
64 |
val local_theory': (xstring * Position.T) option -> (bool -> local_theory -> local_theory) -> |
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset
|
65 |
transition -> transition |
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset
|
66 |
val local_theory: (xstring * Position.T) option -> (local_theory -> local_theory) -> |
29380 | 67 |
transition -> transition |
45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset
|
68 |
val present_local_theory: (xstring * Position.T) option -> (state -> unit) -> |
24453 | 69 |
transition -> transition |
45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset
|
70 |
val local_theory_to_proof': (xstring * Position.T) option -> |
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset
|
71 |
(bool -> local_theory -> Proof.state) -> transition -> transition |
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset
|
72 |
val local_theory_to_proof: (xstring * Position.T) option -> |
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset
|
73 |
(local_theory -> Proof.state) -> transition -> transition |
17363 | 74 |
val theory_to_proof: (theory -> Proof.state) -> transition -> transition |
21007 | 75 |
val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition |
76 |
val forget_proof: transition -> transition |
|
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
77 |
val present_proof: (state -> unit) -> transition -> transition |
49863
b5fb6e7f8d81
more informative errors for 'proof' and 'apply' steps;
wenzelm
parents:
49062
diff
changeset
|
78 |
val proofs': (bool -> Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition |
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset
|
79 |
val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition |
49863
b5fb6e7f8d81
more informative errors for 'proof' and 'apply' steps;
wenzelm
parents:
49062
diff
changeset
|
80 |
val proofs: (Proof.state -> Proof.state Seq.result Seq.seq) -> transition -> transition |
21177 | 81 |
val proof: (Proof.state -> Proof.state) -> transition -> transition |
33390 | 82 |
val actual_proof: (Proof_Node.T -> Proof_Node.T) -> transition -> transition |
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset
|
83 |
val skip_proof: (int -> int) -> transition -> transition |
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset
|
84 |
val skip_proof_to_theory: (int -> bool) -> transition -> transition |
27427 | 85 |
val get_id: transition -> string option |
86 |
val put_id: string -> transition -> transition |
|
9512 | 87 |
val unknown_theory: transition -> transition |
88 |
val unknown_proof: transition -> transition |
|
89 |
val unknown_context: transition -> transition |
|
28425 | 90 |
val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b |
27606 | 91 |
val status: transition -> Markup.T -> unit |
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset
|
92 |
val add_hook: (transition -> state -> state -> unit) -> unit |
51228 | 93 |
val approximative_id: transition -> {file: string, offset: int, name: string} option |
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
94 |
val get_timing: transition -> Time.time option |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
95 |
val put_timing: Time.time option -> transition -> transition |
26602
5534b6a6b810
made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset
|
96 |
val transition: bool -> transition -> state -> (state * (exn * string) option) option |
51323 | 97 |
val command_errors: bool -> transition -> state -> Runtime.error list * state option |
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51282
diff
changeset
|
98 |
val command_exception: bool -> transition -> state -> state |
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
99 |
type result |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
100 |
val join_results: result -> (transition * state) list |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
101 |
val element_result: transition Thy_Syntax.element -> state -> result * state |
5828 | 102 |
end; |
103 |
||
6965 | 104 |
structure Toplevel: TOPLEVEL = |
5828 | 105 |
struct |
106 |
||
107 |
(** toplevel state **) |
|
108 |
||
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset
|
109 |
exception UNDEF = Runtime.UNDEF; |
19063 | 110 |
|
111 |
||
21294 | 112 |
(* local theory wrappers *) |
5828 | 113 |
|
38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38236
diff
changeset
|
114 |
val loc_init = Named_Target.context_cmd; |
47069 | 115 |
val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global; |
21294 | 116 |
|
47274 | 117 |
fun loc_begin loc (Context.Theory thy) = |
118 |
(Context.Theory o loc_exit, loc_init (the_default ("-", Position.none) loc) thy) |
|
119 |
| loc_begin NONE (Context.Proof lthy) = |
|
120 |
(Context.Proof o Local_Theory.restore, lthy) |
|
121 |
| loc_begin (SOME loc) (Context.Proof lthy) = |
|
122 |
(Context.Proof o Named_Target.reinit lthy, loc_init loc (loc_exit lthy)); |
|
21294 | 123 |
|
124 |
||
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset
|
125 |
(* datatype node *) |
21294 | 126 |
|
5828 | 127 |
datatype node = |
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
128 |
Theory of generic_theory * Proof.context option |
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
129 |
(*theory with presentation context*) | |
33390 | 130 |
Proof of Proof_Node.T * ((Proof.context -> generic_theory) * generic_theory) |
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
131 |
(*proof node, finish, original theory*) | |
51555 | 132 |
Skipped_Proof of int * (generic_theory * generic_theory); |
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset
|
133 |
(*proof depth, resulting theory, original theory*) |
5828 | 134 |
|
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
135 |
val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE; |
18589 | 136 |
val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE; |
51555 | 137 |
val skipped_proof_node = fn Skipped_Proof _ => true | _ => false; |
18589 | 138 |
|
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
139 |
fun cases_node f _ (Theory (gthy, _)) = f gthy |
33390 | 140 |
| cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf) |
51555 | 141 |
| cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy; |
19063 | 142 |
|
29066 | 143 |
val context_node = cases_node Context.proof_of Proof.context_of; |
144 |
||
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset
|
145 |
|
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset
|
146 |
(* datatype state *) |
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset
|
147 |
|
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
148 |
datatype state = State of node option * node option; (*current, previous*) |
5828 | 149 |
|
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
150 |
val toplevel = State (NONE, NONE); |
5828 | 151 |
|
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
152 |
fun is_toplevel (State (NONE, _)) = true |
7732 | 153 |
| is_toplevel _ = false; |
154 |
||
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
155 |
fun level (State (NONE, _)) = 0 |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
156 |
| level (State (SOME (Theory _), _)) = 0 |
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
157 |
| level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf) |
51555 | 158 |
| level (State (SOME (Skipped_Proof (d, _)), _)) = d + 1; (*different notion of proof depth!*) |
17076 | 159 |
|
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
160 |
fun str_of_state (State (NONE, _)) = "at top level" |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
161 |
| str_of_state (State (SOME (Theory (Context.Theory _, _)), _)) = "in theory mode" |
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
162 |
| str_of_state (State (SOME (Theory (Context.Proof _, _)), _)) = "in local theory mode" |
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
163 |
| str_of_state (State (SOME (Proof _), _)) = "in proof mode" |
51555 | 164 |
| str_of_state (State (SOME (Skipped_Proof _), _)) = "in skipped proof mode"; |
5946
a4600d21b59b
print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents:
5939
diff
changeset
|
165 |
|
a4600d21b59b
print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents:
5939
diff
changeset
|
166 |
|
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
167 |
(* current node *) |
5828 | 168 |
|
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
169 |
fun node_of (State (NONE, _)) = raise UNDEF |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
170 |
| node_of (State (SOME node, _)) = node; |
5828 | 171 |
|
18589 | 172 |
fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state)); |
173 |
fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state)); |
|
51555 | 174 |
fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state); |
18589 | 175 |
|
19063 | 176 |
fun node_case f g state = cases_node f g (node_of state); |
5828 | 177 |
|
30398 | 178 |
fun presentation_context_of state = |
179 |
(case try node_of state of |
|
180 |
SOME (Theory (_, SOME ctxt)) => ctxt |
|
181 |
| SOME node => context_node node |
|
182 |
| NONE => raise UNDEF); |
|
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
183 |
|
30801 | 184 |
fun previous_context_of (State (_, NONE)) = NONE |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
185 |
| previous_context_of (State (_, SOME prev)) = SOME (context_node prev); |
30801 | 186 |
|
21506 | 187 |
val context_of = node_case Context.proof_of Proof.context_of; |
22089 | 188 |
val generic_theory_of = node_case I (Context.Proof o Proof.context_of); |
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
189 |
val theory_of = node_case Context.theory_of Proof.theory_of; |
18589 | 190 |
val proof_of = node_case (fn _ => raise UNDEF) I; |
17208 | 191 |
|
18589 | 192 |
fun proof_position_of state = |
193 |
(case node_of state of |
|
33390 | 194 |
Proof (prf, _) => Proof_Node.position prf |
18589 | 195 |
| _ => raise UNDEF); |
6664 | 196 |
|
43667
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents:
43665
diff
changeset
|
197 |
fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy |
48992 | 198 |
| end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos) |
199 |
| end_theory pos (State (SOME _, _)) = error ("Unfinished theory" ^ Position.here pos); |
|
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
200 |
|
5828 | 201 |
|
16815 | 202 |
(* print state *) |
203 |
||
38388 | 204 |
val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I; |
16815 | 205 |
|
23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset
|
206 |
fun print_state_context state = |
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset
|
207 |
(case try node_of state of |
21506 | 208 |
NONE => [] |
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset
|
209 |
| SOME (Theory (gthy, _)) => pretty_context gthy |
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset
|
210 |
| SOME (Proof (_, (_, gthy))) => pretty_context gthy |
51555 | 211 |
| SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy) |
23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset
|
212 |
|> Pretty.chunks |> Pretty.writeln; |
16815 | 213 |
|
23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset
|
214 |
fun print_state prf_only state = |
23701 | 215 |
(case try node_of state of |
216 |
NONE => [] |
|
217 |
| SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy |
|
218 |
| SOME (Proof (prf, _)) => |
|
33390 | 219 |
Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf) |
51555 | 220 |
| SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]) |
50201
c26369c9eda6
Isabelle-specific implementation of quasi-abstract markup elements -- back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49863
diff
changeset
|
221 |
|> Pretty.markup_chunks Markup.state |> Pretty.writeln; |
16815 | 222 |
|
37858 | 223 |
fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">"); |
224 |
||
16815 | 225 |
|
15668 | 226 |
|
5828 | 227 |
(** toplevel transitions **) |
228 |
||
32738 | 229 |
val quiet = Unsynchronized.ref false; |
39513
fce2202892c4
discontinued Output.debug, which belongs to early PGIP experiments (b6788dbd2ef9) and causes just too many problems (like spamming the message channel if it is used by more than one module);
wenzelm
parents:
39285
diff
changeset
|
230 |
val debug = Runtime.debug; |
32738 | 231 |
val interact = Unsynchronized.ref false; |
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
41703
diff
changeset
|
232 |
val timing = Unsynchronized.ref false; |
32738 | 233 |
val profiling = Unsynchronized.ref 0; |
16682 | 234 |
|
33604
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
235 |
fun program body = |
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
236 |
(body |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset
|
237 |
|> Runtime.controlled_execution |
33604
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
238 |
|> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) (); |
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
239 |
|
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
240 |
fun thread interrupts body = |
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
241 |
Thread.fork |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
38888
diff
changeset
|
242 |
(((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn) |
33604
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
243 |
|> Runtime.debugging |
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
244 |
|> Runtime.toplevel_error |
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39513
diff
changeset
|
245 |
(fn exn => |
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39513
diff
changeset
|
246 |
Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))), |
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37208
diff
changeset
|
247 |
Simple_Thread.attributes interrupts); |
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset
|
248 |
|
5828 | 249 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
250 |
(* node transactions -- maintaining stable checkpoints *) |
7022 | 251 |
|
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset
|
252 |
exception FAILURE of state * exn; |
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset
|
253 |
|
6689 | 254 |
local |
255 |
||
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
256 |
fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE) |
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
257 |
| reset_presentation node = node; |
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
258 |
|
26624
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
259 |
fun is_draft_theory (Theory (gthy, _)) = Context.is_draft (Context.theory_of gthy) |
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
260 |
| is_draft_theory _ = false; |
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
261 |
|
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset
|
262 |
fun is_stale state = Context.is_stale (theory_of state) handle Runtime.UNDEF => false; |
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
263 |
|
26624
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
264 |
fun stale_error NONE = SOME (ERROR "Stale theory encountered after successful execution!") |
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
265 |
| stale_error some = some; |
16815 | 266 |
|
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
267 |
fun map_theory f (Theory (gthy, ctxt)) = |
33671 | 268 |
Theory (Context.mapping f (Local_Theory.raw_theory f) gthy, ctxt) |
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
269 |
| map_theory _ node = node; |
6689 | 270 |
|
271 |
in |
|
272 |
||
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
273 |
fun apply_transaction f g node = |
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset
|
274 |
let |
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
275 |
val _ = is_draft_theory node andalso error "Illegal draft theory in toplevel state"; |
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
276 |
val cont_node = reset_presentation node; |
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
277 |
val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node; |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
278 |
fun state_error e nd = (State (SOME nd, SOME node), e); |
6689 | 279 |
|
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset
|
280 |
val (result, err) = |
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset
|
281 |
cont_node |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset
|
282 |
|> Runtime.controlled_execution f |
26624
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
283 |
|> map_theory Theory.checkpoint |
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
284 |
|> state_error NONE |
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
285 |
handle exn => state_error (SOME exn) cont_node; |
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
286 |
|
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
287 |
val (result', err') = |
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
288 |
if is_stale result then state_error (stale_error err) back_node |
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
289 |
else (result, err); |
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset
|
290 |
in |
26624
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
291 |
(case err' of |
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
292 |
NONE => tap g result' |
26624
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
293 |
| SOME exn => raise FAILURE (result', exn)) |
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset
|
294 |
end; |
6689 | 295 |
|
43667
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents:
43665
diff
changeset
|
296 |
val exit_transaction = |
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents:
43665
diff
changeset
|
297 |
apply_transaction |
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents:
43665
diff
changeset
|
298 |
(fn Theory (Context.Theory thy, _) => Theory (Context.Theory (Theory.end_theory thy), NONE) |
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents:
43665
diff
changeset
|
299 |
| node => node) (K ()) |
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents:
43665
diff
changeset
|
300 |
#> (fn State (node', _) => State (NONE, node')); |
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents:
43665
diff
changeset
|
301 |
|
6689 | 302 |
end; |
303 |
||
304 |
||
305 |
(* primitive transitions *) |
|
306 |
||
5828 | 307 |
datatype trans = |
44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset
|
308 |
Init of unit -> theory | (*init theory*) |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
309 |
Exit | (*formal exit of theory*) |
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
310 |
Keep of bool -> state -> unit | (*peek at state*) |
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
311 |
Transaction of (bool -> node -> node) * (state -> unit); (*node transaction and presentation*) |
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset
|
312 |
|
6689 | 313 |
local |
5828 | 314 |
|
44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset
|
315 |
fun apply_tr _ (Init f) (State (NONE, _)) = |
33727
e2d5d7f51aa3
init_theory: Runtime.controlled_execution for proper exception trace etc.;
wenzelm
parents:
33725
diff
changeset
|
316 |
State (SOME (Theory (Context.Theory |
44186
806f0ec1a43d
simplified Toplevel.init_theory: discontinued special master argument;
wenzelm
parents:
44185
diff
changeset
|
317 |
(Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE) |
43667
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents:
43665
diff
changeset
|
318 |
| apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) = |
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOL-SPARK for example);
wenzelm
parents:
43665
diff
changeset
|
319 |
exit_transaction state |
32792 | 320 |
| apply_tr int (Keep f) state = |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset
|
321 |
Runtime.controlled_execution (fn x => tap (f int) x) state |
32792 | 322 |
| apply_tr int (Transaction (f, g)) (State (SOME state, _)) = |
323 |
apply_transaction (fn x => f int x) g state |
|
324 |
| apply_tr _ _ _ = raise UNDEF; |
|
5828 | 325 |
|
32792 | 326 |
fun apply_union _ [] state = raise FAILURE (state, UNDEF) |
327 |
| apply_union int (tr :: trs) state = |
|
328 |
apply_union int trs state |
|
329 |
handle Runtime.UNDEF => apply_tr int tr state |
|
330 |
| FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state |
|
6689 | 331 |
| exn as FAILURE _ => raise exn |
332 |
| exn => raise FAILURE (state, exn); |
|
333 |
||
334 |
in |
|
335 |
||
32792 | 336 |
fun apply_trans int trs state = (apply_union int trs state, NONE) |
15531 | 337 |
handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn); |
6689 | 338 |
|
339 |
end; |
|
5828 | 340 |
|
341 |
||
342 |
(* datatype transition *) |
|
343 |
||
344 |
datatype transition = Transition of |
|
26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
345 |
{name: string, (*command name*) |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
346 |
pos: Position.T, (*source position*) |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
347 |
int_only: bool, (*interactive-only*) |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
348 |
print: bool, (*print result state*) |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
349 |
no_timing: bool, (*suppress timing*) |
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
350 |
timing: Time.time option, (*prescient timing information*) |
26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
351 |
trans: trans list}; (*primitive transitions (union)*) |
5828 | 352 |
|
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
353 |
fun make_transition (name, pos, int_only, print, no_timing, timing, trans) = |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
354 |
Transition {name = name, pos = pos, int_only = int_only, print = print, |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
355 |
no_timing = no_timing, timing = timing, trans = trans}; |
5828 | 356 |
|
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
357 |
fun map_transition f (Transition {name, pos, int_only, print, no_timing, timing, trans}) = |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
358 |
make_transition (f (name, pos, int_only, print, no_timing, timing, trans)); |
5828 | 359 |
|
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
360 |
val empty = make_transition ("", Position.none, false, false, false, NONE, []); |
5828 | 361 |
|
362 |
||
363 |
(* diagnostics *) |
|
364 |
||
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset
|
365 |
fun print_of (Transition {print, ...}) = print; |
27427 | 366 |
fun name_of (Transition {name, ...}) = name; |
28105 | 367 |
fun pos_of (Transition {pos, ...}) = pos; |
5828 | 368 |
|
48993 | 369 |
fun command_msg msg tr = msg ^ "command " ^ quote (name_of tr) ^ Position.here (pos_of tr); |
38875
c7a66b584147
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
wenzelm
parents:
38721
diff
changeset
|
370 |
fun at_command tr = command_msg "At " tr; |
5828 | 371 |
|
372 |
fun type_error tr state = |
|
18685 | 373 |
ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); |
5828 | 374 |
|
375 |
||
376 |
(* modify transitions *) |
|
377 |
||
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
378 |
fun name name = map_transition (fn (_, pos, int_only, print, no_timing, timing, trans) => |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
379 |
(name, pos, int_only, print, no_timing, timing, trans)); |
9010 | 380 |
|
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
381 |
fun position pos = map_transition (fn (name, _, int_only, print, no_timing, timing, trans) => |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
382 |
(name, pos, int_only, print, no_timing, timing, trans)); |
5828 | 383 |
|
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
384 |
fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, timing, trans) => |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
385 |
(name, pos, int_only, print, no_timing, timing, trans)); |
14923 | 386 |
|
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
387 |
val no_timing = map_transition (fn (name, pos, int_only, print, _, timing, trans) => |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
388 |
(name, pos, int_only, print, true, timing, trans)); |
17363 | 389 |
|
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
390 |
fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, timing, trans) => |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
391 |
(name, pos, int_only, print, no_timing, timing, tr :: trans)); |
16607 | 392 |
|
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
393 |
val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, timing, _) => |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
394 |
(name, pos, int_only, print, no_timing, timing, [])); |
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
395 |
|
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
396 |
fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, timing, trans) => |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
397 |
(name, pos, int_only, print, no_timing, timing, trans)); |
28453
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset
|
398 |
|
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset
|
399 |
val print = set_print true; |
5828 | 400 |
|
401 |
||
21007 | 402 |
(* basic transitions *) |
5828 | 403 |
|
44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset
|
404 |
fun init_theory f = add_trans (Init f); |
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37953
diff
changeset
|
405 |
|
44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset
|
406 |
fun is_init (Transition {trans = [Init _], ...}) = true |
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset
|
407 |
| is_init _ = false; |
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset
|
408 |
|
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset
|
409 |
fun modify_init f tr = if is_init tr then init_theory f (reset_trans tr) else tr; |
37977
3ceccd415145
simplified/clarified theory loader: more explicit task management, kill old versions at start, commit results only in the very end, non-optional master dependency, do not store text in deps;
wenzelm
parents:
37953
diff
changeset
|
410 |
|
6689 | 411 |
val exit = add_trans Exit; |
7612 | 412 |
val keep' = add_trans o Keep; |
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
413 |
|
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
414 |
fun present_transaction f g = add_trans (Transaction (f, g)); |
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
415 |
fun transaction f = present_transaction f (K ()); |
5828 | 416 |
|
7612 | 417 |
fun keep f = add_trans (Keep (fn _ => f)); |
5828 | 418 |
fun imperative f = keep (fn _ => f ()); |
419 |
||
27840 | 420 |
fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I; |
51268
fcc4b89a600d
simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
wenzelm
parents:
51241
diff
changeset
|
421 |
fun is_ignored tr = name_of tr = "<ignored>"; |
48772 | 422 |
|
423 |
val malformed_name = "<malformed>"; |
|
27840 | 424 |
fun malformed pos msg = |
48772 | 425 |
empty |> name malformed_name |> position pos |> imperative (fn () => error msg); |
426 |
fun is_malformed tr = name_of tr = malformed_name; |
|
27840 | 427 |
|
21007 | 428 |
val unknown_theory = imperative (fn () => warning "Unknown theory context"); |
429 |
val unknown_proof = imperative (fn () => warning "Unknown proof context"); |
|
430 |
val unknown_context = imperative (fn () => warning "Unknown context"); |
|
15668 | 431 |
|
21007 | 432 |
|
49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset
|
433 |
(* theory transitions *) |
44304
7ee000ce5390
maintain recent future proofs at transaction boundaries;
wenzelm
parents:
44270
diff
changeset
|
434 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
435 |
fun generic_theory f = transaction (fn _ => |
26491 | 436 |
(fn Theory (gthy, _) => Theory (f gthy, NONE) |
437 |
| _ => raise UNDEF)); |
|
438 |
||
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
439 |
fun theory' f = transaction (fn int => |
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
440 |
(fn Theory (Context.Theory thy, _) => |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
441 |
let val thy' = thy |
49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset
|
442 |
|> Sign.new_group |
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset
|
443 |
|> Theory.checkpoint |
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
444 |
|> f int |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
445 |
|> Sign.reset_group; |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
446 |
in Theory (Context.Theory thy', NONE) end |
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
447 |
| _ => raise UNDEF)); |
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
448 |
|
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
449 |
fun theory f = theory' (K f); |
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
450 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
451 |
fun begin_local_theory begin f = transaction (fn _ => |
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
452 |
(fn Theory (Context.Theory thy, _) => |
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
453 |
let |
20985 | 454 |
val lthy = f thy; |
21294 | 455 |
val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy); |
456 |
in Theory (gthy, SOME lthy) end |
|
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
457 |
| _ => raise UNDEF)); |
17076 | 458 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
459 |
val end_local_theory = transaction (fn _ => |
21294 | 460 |
(fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy) |
21007 | 461 |
| _ => raise UNDEF)); |
462 |
||
47069 | 463 |
fun open_target f = transaction (fn _ => |
464 |
(fn Theory (gthy, _) => |
|
465 |
let val lthy = f gthy |
|
466 |
in Theory (Context.Proof lthy, SOME lthy) end |
|
467 |
| _ => raise UNDEF)); |
|
468 |
||
469 |
val close_target = transaction (fn _ => |
|
470 |
(fn Theory (Context.Proof lthy, _) => |
|
471 |
(case try Local_Theory.close_target lthy of |
|
50739
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50201
diff
changeset
|
472 |
SOME ctxt' => |
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50201
diff
changeset
|
473 |
let |
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50201
diff
changeset
|
474 |
val gthy' = |
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50201
diff
changeset
|
475 |
if can Local_Theory.assert ctxt' |
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50201
diff
changeset
|
476 |
then Context.Proof ctxt' |
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50201
diff
changeset
|
477 |
else Context.Theory (Proof_Context.theory_of ctxt'); |
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50201
diff
changeset
|
478 |
in Theory (gthy', SOME lthy) end |
47069 | 479 |
| NONE => raise UNDEF) |
480 |
| _ => raise UNDEF)); |
|
481 |
||
482 |
||
21007 | 483 |
local |
484 |
||
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
485 |
fun local_theory_presentation loc f = present_transaction (fn int => |
21294 | 486 |
(fn Theory (gthy, _) => |
487 |
let |
|
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49042
diff
changeset
|
488 |
val (finish, lthy) = loc_begin loc gthy; |
47274 | 489 |
val lthy' = lthy |
49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset
|
490 |
|> Local_Theory.new_group |
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
491 |
|> f int |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
492 |
|> Local_Theory.reset_group; |
21294 | 493 |
in Theory (finish lthy', SOME lthy') end |
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
494 |
| _ => raise UNDEF)); |
15668 | 495 |
|
21007 | 496 |
in |
497 |
||
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
498 |
fun local_theory' loc f = local_theory_presentation loc f (K ()); |
29380 | 499 |
fun local_theory loc f = local_theory' loc (K f); |
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
500 |
fun present_local_theory loc = local_theory_presentation loc (K I); |
18955 | 501 |
|
21007 | 502 |
end; |
503 |
||
504 |
||
505 |
(* proof transitions *) |
|
506 |
||
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
507 |
fun end_proof f = transaction (fn int => |
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset
|
508 |
(fn Proof (prf, (finish, _)) => |
33390 | 509 |
let val state = Proof_Node.current prf in |
21007 | 510 |
if can (Proof.assert_bottom true) state then |
511 |
let |
|
512 |
val ctxt' = f int state; |
|
513 |
val gthy' = finish ctxt'; |
|
514 |
in Theory (gthy', SOME ctxt') end |
|
515 |
else raise UNDEF |
|
516 |
end |
|
51555 | 517 |
| Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE) |
21007 | 518 |
| _ => raise UNDEF)); |
519 |
||
21294 | 520 |
local |
521 |
||
47274 | 522 |
fun begin_proof init = transaction (fn int => |
21294 | 523 |
(fn Theory (gthy, _) => |
524 |
let |
|
47274 | 525 |
val (finish, prf) = init int gthy; |
51553
63327f679cff
more ambitious Goal.skip_proofs: covers Goal.prove forms as well, and do not insist in quick_and_dirty (for the sake of Isabelle/jEdit);
wenzelm
parents:
51423
diff
changeset
|
526 |
val skip = ! Goal.skip_proofs; |
40960 | 527 |
val (is_goal, no_skip) = |
528 |
(true, Proof.schematic_goal prf) handle ERROR _ => (false, true); |
|
47274 | 529 |
val _ = |
530 |
if is_goal andalso skip andalso no_skip then |
|
531 |
warning "Cannot skip proof of schematic goal statement" |
|
532 |
else (); |
|
21294 | 533 |
in |
40960 | 534 |
if skip andalso not no_skip then |
51555 | 535 |
Skipped_Proof (0, (finish (Proof.global_skip_proof true prf), gthy)) |
47274 | 536 |
else Proof (Proof_Node.init prf, (finish, gthy)) |
21294 | 537 |
end |
538 |
| _ => raise UNDEF)); |
|
539 |
||
540 |
in |
|
541 |
||
24780
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset
|
542 |
fun local_theory_to_proof' loc f = begin_proof |
47274 | 543 |
(fn int => fn gthy => |
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49042
diff
changeset
|
544 |
let val (finish, lthy) = loc_begin loc gthy |
49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset
|
545 |
in (finish o Local_Theory.reset_group, f int (Local_Theory.new_group lthy)) end); |
24780
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset
|
546 |
|
24453 | 547 |
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f); |
21294 | 548 |
|
549 |
fun theory_to_proof f = begin_proof |
|
47274 | 550 |
(fn _ => fn gthy => |
51560
5b4ae2467830
extra checkpoint to avoid stale theory in skip_proof context, e.g. in 'instance' proof;
wenzelm
parents:
51555
diff
changeset
|
551 |
(Context.Theory o Theory.checkpoint o Sign.reset_group o Proof_Context.theory_of, |
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49042
diff
changeset
|
552 |
(case gthy of |
49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset
|
553 |
Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) |
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset
|
554 |
| _ => raise UNDEF))); |
21294 | 555 |
|
556 |
end; |
|
557 |
||
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
558 |
val forget_proof = transaction (fn _ => |
21007 | 559 |
(fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) |
51555 | 560 |
| Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) |
21007 | 561 |
| _ => raise UNDEF)); |
562 |
||
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
563 |
val present_proof = present_transaction (fn _ => |
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49042
diff
changeset
|
564 |
(fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x) |
51555 | 565 |
| skip as Skipped_Proof _ => skip |
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
566 |
| _ => raise UNDEF)); |
21177 | 567 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
568 |
fun proofs' f = transaction (fn int => |
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49042
diff
changeset
|
569 |
(fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) |
51555 | 570 |
| skip as Skipped_Proof _ => skip |
16815 | 571 |
| _ => raise UNDEF)); |
15668 | 572 |
|
49863
b5fb6e7f8d81
more informative errors for 'proof' and 'apply' steps;
wenzelm
parents:
49062
diff
changeset
|
573 |
fun proof' f = proofs' ((Seq.single o Seq.Result) oo f); |
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset
|
574 |
val proofs = proofs' o K; |
6689 | 575 |
val proof = proof' o K; |
16815 | 576 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
577 |
fun actual_proof f = transaction (fn _ => |
21007 | 578 |
(fn Proof (prf, x) => Proof (f prf, x) |
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
579 |
| _ => raise UNDEF)); |
16815 | 580 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
581 |
fun skip_proof f = transaction (fn _ => |
51555 | 582 |
(fn Skipped_Proof (h, x) => Skipped_Proof (f h, x) |
18563 | 583 |
| _ => raise UNDEF)); |
584 |
||
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
585 |
fun skip_proof_to_theory pred = transaction (fn _ => |
51555 | 586 |
(fn Skipped_Proof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF |
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
587 |
| _ => raise UNDEF)); |
5828 | 588 |
|
589 |
||
590 |
||
591 |
(** toplevel transactions **) |
|
592 |
||
27427 | 593 |
(* identification *) |
594 |
||
595 |
fun get_id (Transition {pos, ...}) = Position.get_id pos; |
|
596 |
fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr; |
|
597 |
||
598 |
||
51228 | 599 |
(* approximative identification within source file *) |
600 |
||
601 |
fun approximative_id tr = |
|
602 |
let |
|
603 |
val name = name_of tr; |
|
604 |
val pos = pos_of tr; |
|
605 |
in |
|
606 |
(case (Position.file_of pos, Position.offset_of pos) of |
|
607 |
(SOME file, SOME offset) => SOME {file = file, offset = offset, name = name} |
|
608 |
| _ => NONE) |
|
609 |
end; |
|
610 |
||
611 |
||
25960 | 612 |
(* thread position *) |
25799 | 613 |
|
25960 | 614 |
fun setmp_thread_position (Transition {pos, ...}) f x = |
25819
e6feb08b7f4b
replaced thread_properties by simplified version in position.ML;
wenzelm
parents:
25809
diff
changeset
|
615 |
Position.setmp_thread_data pos f x; |
25799 | 616 |
|
27606 | 617 |
fun status tr m = |
43665 | 618 |
setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) (); |
27606 | 619 |
|
25799 | 620 |
|
28095
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
621 |
(* post-transition hooks *) |
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
622 |
|
37905 | 623 |
local |
624 |
val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list); |
|
625 |
in |
|
28095
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
626 |
|
32738 | 627 |
fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f)); |
33223 | 628 |
fun get_hooks () = ! hooks; |
28095
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
629 |
|
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
630 |
end; |
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
631 |
|
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
632 |
|
5828 | 633 |
(* apply transitions *) |
634 |
||
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
635 |
fun get_timing (Transition {timing, ...}) = timing; |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
636 |
fun put_timing timing = map_transition (fn (name, pos, int_only, print, no_timing, _, trans) => |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
637 |
(name, pos, int_only, print, no_timing, timing, trans)); |
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset
|
638 |
|
6664 | 639 |
local |
640 |
||
51241 | 641 |
fun timing_message tr (t: Timing.timing) = |
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
642 |
(case approximative_id tr of |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
643 |
SOME id => |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
644 |
(Output.protocol_message |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
645 |
(Markup.command_timing :: Markup.command_timing_properties id (#elapsed t)) "" |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
646 |
handle Fail _ => ()) |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
647 |
| NONE => ()); |
51216 | 648 |
|
32792 | 649 |
fun app int (tr as Transition {trans, print, no_timing, ...}) = |
25819
e6feb08b7f4b
replaced thread_properties by simplified version in position.ML;
wenzelm
parents:
25809
diff
changeset
|
650 |
setmp_thread_position tr (fn state => |
25799 | 651 |
let |
652 |
fun do_timing f x = (warning (command_msg "" tr); timeap f x); |
|
653 |
fun do_profiling f x = profile (! profiling) f x; |
|
654 |
||
51216 | 655 |
val start = Timing.start (); |
656 |
||
26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset
|
657 |
val (result, status) = |
37905 | 658 |
state |> |
659 |
(apply_trans int trans |
|
660 |
|> (! profiling > 0 andalso not no_timing) ? do_profiling |
|
661 |
|> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing); |
|
26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset
|
662 |
|
26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
663 |
val _ = if int andalso not (! quiet) andalso print then print_state false result else (); |
51216 | 664 |
|
665 |
val _ = timing_message tr (Timing.result start); |
|
26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset
|
666 |
in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end); |
6664 | 667 |
|
668 |
in |
|
5828 | 669 |
|
26602
5534b6a6b810
made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset
|
670 |
fun transition int tr st = |
28095
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
671 |
let |
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
672 |
val hooks = get_hooks (); |
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset
|
673 |
fun apply_hooks st' = hooks |> List.app (fn f => (try (fn () => f tr st st') (); ())); |
28095
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
674 |
|
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
675 |
val ctxt = try context_of st; |
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
676 |
val res = |
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
677 |
(case app int tr st of |
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset
|
678 |
(_, SOME Runtime.TERMINATE) => NONE |
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset
|
679 |
| (st', SOME (Runtime.EXCURSION_FAIL exn_info)) => SOME (st', SOME exn_info) |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset
|
680 |
| (st', SOME exn) => SOME (st', SOME (Runtime.exn_context ctxt exn, at_command tr)) |
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset
|
681 |
| (st', NONE) => SOME (st', NONE)); |
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset
|
682 |
val _ = (case res of SOME (st', NONE) => apply_hooks st' | _ => ()); |
28095
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
683 |
in res end; |
6664 | 684 |
|
685 |
end; |
|
5828 | 686 |
|
687 |
||
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51282
diff
changeset
|
688 |
(* managed commands *) |
5828 | 689 |
|
51323 | 690 |
fun command_errors int tr st = |
691 |
(case transition int tr st of |
|
692 |
SOME (st', NONE) => ([], SOME st') |
|
693 |
| SOME (_, SOME (exn, _)) => (ML_Compiler.exn_messages_ids exn, NONE) |
|
694 |
| NONE => (ML_Compiler.exn_messages_ids Runtime.TERMINATE, NONE)); |
|
695 |
||
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51282
diff
changeset
|
696 |
fun command_exception int tr st = |
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51282
diff
changeset
|
697 |
(case transition int tr st of |
28425 | 698 |
SOME (st', NONE) => st' |
39285 | 699 |
| SOME (_, SOME (exn, info)) => |
700 |
if Exn.is_interrupt exn then reraise exn else raise Runtime.EXCURSION_FAIL (exn, info) |
|
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset
|
701 |
| NONE => raise Runtime.EXCURSION_FAIL (Runtime.TERMINATE, at_command tr)); |
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
702 |
|
51323 | 703 |
fun command tr = command_exception (! interact) tr; |
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51282
diff
changeset
|
704 |
|
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
705 |
|
46959
cdc791910460
defer actual parsing of command spans and thus allow new commands to be used in the same theory where defined;
wenzelm
parents:
45666
diff
changeset
|
706 |
(* scheduled proof result *) |
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
707 |
|
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
708 |
datatype result = |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
709 |
Result of transition * state | |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
710 |
Result_List of result list | |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
711 |
Result_Future of result future; |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
712 |
|
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
713 |
fun join_results (Result x) = [x] |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
714 |
| join_results (Result_List xs) = maps join_results xs |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
715 |
| join_results (Result_Future x) = join_results (Future.join x); |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
716 |
|
51323 | 717 |
local |
718 |
||
47417 | 719 |
structure Result = Proof_Data |
28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset
|
720 |
( |
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
721 |
type T = result; |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
722 |
val empty: T = Result_List []; |
47417 | 723 |
fun init _ = empty; |
28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset
|
724 |
); |
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset
|
725 |
|
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
726 |
val get_result = Result.get o Proof.context_of; |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
727 |
val put_result = Proof.map_context o Result.put; |
51324 | 728 |
|
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
729 |
fun timing_estimate include_head elem = |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
730 |
let |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
731 |
val trs = Thy_Syntax.flat_element elem |> not include_head ? tl; |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
732 |
val timings = map get_timing trs; |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
733 |
in |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
734 |
if forall is_some timings then |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
735 |
SOME (fold (curry Time.+ o the) timings Time.zeroTime) |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
736 |
else NONE |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
737 |
end; |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
738 |
|
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
739 |
fun priority NONE = ~1 |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
740 |
| priority (SOME estimate) = |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
741 |
Int.min (Real.floor (Real.max (Math.log10 (Time.toReal estimate), ~3.0)) - 3, ~1); |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
742 |
|
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
743 |
fun proof_future_enabled estimate st = |
51324 | 744 |
(case try proof_of st of |
745 |
NONE => false |
|
746 |
| SOME state => |
|
747 |
not (Proof.is_relevant state) andalso |
|
748 |
(if can (Proof.assert_bottom true) state |
|
749 |
then Goal.future_enabled () |
|
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
750 |
else |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
751 |
(case estimate of |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
752 |
NONE => Goal.future_enabled_nested 2 |
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
753 |
| SOME t => Goal.future_enabled_timing t))); |
51278 | 754 |
|
51323 | 755 |
fun atom_result tr st = |
756 |
let |
|
757 |
val st' = |
|
758 |
if Goal.future_enabled () andalso Keyword.is_diag (name_of tr) then |
|
759 |
setmp_thread_position tr (fn () => |
|
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
760 |
(Goal.fork_name "Toplevel.diag" (priority (timing_estimate true (Thy_Syntax.atom tr))) |
51323 | 761 |
(fn () => command tr st); st)) () |
762 |
else command tr st; |
|
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
763 |
in (Result (tr, st'), st') end; |
51323 | 764 |
|
765 |
in |
|
766 |
||
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
767 |
fun element_result (Thy_Syntax.Element (tr, NONE)) st = atom_result tr st |
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
768 |
| element_result (elem as Thy_Syntax.Element (head_tr, SOME element_rest)) st = |
48633
7cd32f9d4293
recovered comination of Toplevel.skip_proofs and Goal.parallel_proofs from 9679bab23f93 (NB: skip_proofs leads to failure of Toplevel.proof_of);
wenzelm
parents:
47881
diff
changeset
|
769 |
let |
51324 | 770 |
val (head_result, st') = atom_result head_tr st; |
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
771 |
val (body_elems, end_tr) = element_rest; |
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
772 |
val estimate = timing_estimate false elem; |
51324 | 773 |
in |
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
774 |
if not (proof_future_enabled estimate st') |
51324 | 775 |
then |
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
776 |
let |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
777 |
val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr]; |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
778 |
val (proof_results, st'') = fold_map atom_result proof_trs st'; |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
779 |
in (Result_List (head_result :: proof_results), st'') end |
51324 | 780 |
else |
781 |
let |
|
782 |
val finish = Context.Theory o Proof_Context.theory_of; |
|
28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset
|
783 |
|
51324 | 784 |
val future_proof = Proof.future_proof |
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
785 |
(fn state => |
51324 | 786 |
setmp_thread_position head_tr (fn () => |
787 |
Goal.fork_name "Toplevel.future_proof" |
|
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset
|
788 |
(priority estimate) |
51324 | 789 |
(fn () => |
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
790 |
let |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
791 |
val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st'; |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
792 |
val prf' = Proof_Node.apply (K state) prf; |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
793 |
val (result, result_state) = |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
794 |
State (SOME (Proof (prf', (finish, orig_gthy))), prev) |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
795 |
|> fold_map element_result body_elems ||> command end_tr; |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
796 |
in (Result_List result, presentation_context_of result_state) end)) ()) |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
797 |
#> (fn (res, state') => state' |> put_result (Result_Future res)); |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
798 |
|
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
799 |
val forked_proof = |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
800 |
proof (future_proof #> |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
801 |
(fn state => state |> Proof.local_done_proof |> put_result (get_result state))) o |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
802 |
end_proof (fn _ => future_proof #> |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
803 |
(fn state => state |> Proof.global_done_proof |> Result.put (get_result state))); |
28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced low-level Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset
|
804 |
|
51324 | 805 |
val st'' = st' |
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
806 |
|> command (head_tr |> set_print false |> reset_trans |> forked_proof); |
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
807 |
val end_result = Result (end_tr, st''); |
51324 | 808 |
val result = |
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar sub-proofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset
|
809 |
Result_List [head_result, Result.get (presentation_context_of st''), end_result]; |
51324 | 810 |
in (result, st'') end |
811 |
end; |
|
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
812 |
|
6664 | 813 |
end; |
51323 | 814 |
|
815 |
end; |