author | wenzelm |
Sat, 04 Dec 2010 21:26:55 +0100 | |
changeset 40960 | 9e54eb514a46 |
parent 40132 | 7ee65dbffa31 |
child 41536 | 47fef6afe756 |
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 |
|
17076 | 15 |
val level: state -> int |
30398 | 16 |
val presentation_context_of: state -> Proof.context |
30801 | 17 |
val previous_context_of: state -> Proof.context option |
21506 | 18 |
val context_of: state -> Proof.context |
22089 | 19 |
val generic_theory_of: state -> generic_theory |
5828 | 20 |
val theory_of: state -> theory |
21 |
val proof_of: state -> Proof.state |
|
18589 | 22 |
val proof_position_of: state -> int |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
23 |
val end_theory: Position.T -> state -> theory |
16815 | 24 |
val print_state_context: state -> unit |
25 |
val print_state: bool -> state -> unit |
|
37858 | 26 |
val pretty_abstract: state -> Pretty.T |
32738 | 27 |
val quiet: bool Unsynchronized.ref |
28 |
val debug: bool Unsynchronized.ref |
|
29 |
val interact: bool Unsynchronized.ref |
|
30 |
val timing: bool Unsynchronized.ref |
|
31 |
val profiling: int Unsynchronized.ref |
|
32 |
val skip_proofs: bool 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 |
27441 | 37 |
val init_of: transition -> string option |
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset
|
38 |
val print_of: transition -> bool |
27427 | 39 |
val name_of: transition -> string |
28105 | 40 |
val pos_of: transition -> Position.T |
27500 | 41 |
val str_of: transition -> string |
5828 | 42 |
val name: string -> transition -> transition |
43 |
val position: Position.T -> transition -> transition |
|
44 |
val interactive: bool -> transition -> transition |
|
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset
|
45 |
val set_print: bool -> transition -> transition |
5828 | 46 |
val print: transition -> transition |
9010 | 47 |
val no_timing: transition -> transition |
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
|
48 |
val init_theory: string -> (unit -> theory) -> transition -> transition |
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
|
49 |
val modify_init: (unit -> theory) -> transition -> transition |
6689 | 50 |
val exit: transition -> transition |
5828 | 51 |
val keep: (state -> unit) -> transition -> transition |
7612 | 52 |
val keep': (bool -> state -> unit) -> transition -> transition |
5828 | 53 |
val imperative: (unit -> unit) -> transition -> transition |
27840 | 54 |
val ignored: Position.T -> transition |
55 |
val malformed: Position.T -> string -> transition |
|
5828 | 56 |
val theory: (theory -> theory) -> transition -> transition |
26491 | 57 |
val generic_theory: (generic_theory -> generic_theory) -> transition -> transition |
7612 | 58 |
val theory': (bool -> theory -> theory) -> transition -> transition |
20985 | 59 |
val begin_local_theory: bool -> (theory -> local_theory) -> transition -> transition |
21007 | 60 |
val end_local_theory: transition -> transition |
29380 | 61 |
val local_theory': xstring option -> (bool -> local_theory -> local_theory) -> |
62 |
transition -> transition |
|
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
63 |
val local_theory: xstring option -> (local_theory -> local_theory) -> transition -> transition |
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
64 |
val present_local_theory: xstring option -> (state -> unit) -> transition -> transition |
24453 | 65 |
val local_theory_to_proof': xstring option -> (bool -> local_theory -> Proof.state) -> |
66 |
transition -> transition |
|
21007 | 67 |
val local_theory_to_proof: xstring option -> (local_theory -> Proof.state) -> |
68 |
transition -> transition |
|
17363 | 69 |
val theory_to_proof: (theory -> Proof.state) -> transition -> transition |
21007 | 70 |
val end_proof: (bool -> Proof.state -> Proof.context) -> transition -> transition |
71 |
val forget_proof: transition -> transition |
|
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
72 |
val present_proof: (state -> unit) -> transition -> transition |
21177 | 73 |
val proofs': (bool -> Proof.state -> Proof.state Seq.seq) -> transition -> transition |
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset
|
74 |
val proof': (bool -> Proof.state -> Proof.state) -> transition -> transition |
21177 | 75 |
val proofs: (Proof.state -> Proof.state Seq.seq) -> transition -> transition |
76 |
val proof: (Proof.state -> Proof.state) -> transition -> transition |
|
33390 | 77 |
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
|
78 |
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
|
79 |
val skip_proof_to_theory: (int -> bool) -> transition -> transition |
27427 | 80 |
val get_id: transition -> string option |
81 |
val put_id: string -> transition -> transition |
|
9512 | 82 |
val unknown_theory: transition -> transition |
83 |
val unknown_proof: transition -> transition |
|
84 |
val unknown_context: transition -> transition |
|
28425 | 85 |
val setmp_thread_position: transition -> ('a -> 'b) -> 'a -> 'b |
27606 | 86 |
val status: transition -> Markup.T -> unit |
38876
ec7045139e70
Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
wenzelm
parents:
38875
diff
changeset
|
87 |
val error_msg: transition -> string -> unit |
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset
|
88 |
val add_hook: (transition -> state -> state -> unit) -> unit |
26602
5534b6a6b810
made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset
|
89 |
val transition: bool -> transition -> state -> (state * (exn * string) option) option |
28425 | 90 |
val command: transition -> state -> state |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
91 |
val excursion: (transition * transition list) list -> (transition * state) list lazy * theory |
5828 | 92 |
end; |
93 |
||
6965 | 94 |
structure Toplevel: TOPLEVEL = |
5828 | 95 |
struct |
96 |
||
97 |
(** toplevel state **) |
|
98 |
||
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset
|
99 |
exception UNDEF = Runtime.UNDEF; |
19063 | 100 |
|
101 |
||
21294 | 102 |
(* local theory wrappers *) |
5828 | 103 |
|
38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38236
diff
changeset
|
104 |
val loc_init = Named_Target.context_cmd; |
33671 | 105 |
val loc_exit = Local_Theory.exit_global; |
21294 | 106 |
|
25292 | 107 |
fun loc_begin loc (Context.Theory thy) = loc_init (the_default "-" loc) thy |
21294 | 108 |
| loc_begin NONE (Context.Proof lthy) = lthy |
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
109 |
| loc_begin (SOME loc) (Context.Proof lthy) = (loc_init loc o loc_exit) lthy; |
21294 | 110 |
|
111 |
fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit |
|
33671 | 112 |
| loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore |
38391
ba1cc1815ce1
named target is optional; explicit Name_Target.reinit
haftmann
parents:
38389
diff
changeset
|
113 |
| loc_finish (SOME _) (Context.Proof lthy) = Context.Proof o Named_Target.reinit lthy; |
21294 | 114 |
|
115 |
||
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset
|
116 |
(* datatype node *) |
21294 | 117 |
|
5828 | 118 |
datatype node = |
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
119 |
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
|
120 |
(*theory with presentation context*) | |
33390 | 121 |
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
|
122 |
(*proof node, finish, original theory*) | |
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset
|
123 |
SkipProof of int * (generic_theory * generic_theory); |
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset
|
124 |
(*proof depth, resulting theory, original theory*) |
5828 | 125 |
|
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
126 |
val theory_node = fn Theory (gthy, _) => SOME gthy | _ => NONE; |
18589 | 127 |
val proof_node = fn Proof (prf, _) => SOME prf | _ => NONE; |
128 |
||
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
129 |
fun cases_node f _ (Theory (gthy, _)) = f gthy |
33390 | 130 |
| cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf) |
21007 | 131 |
| cases_node f _ (SkipProof (_, (gthy, _))) = f gthy; |
19063 | 132 |
|
29066 | 133 |
val context_node = cases_node Context.proof_of Proof.context_of; |
134 |
||
21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset
|
135 |
|
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset
|
136 |
(* datatype state *) |
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset
|
137 |
|
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
138 |
datatype state = State of node option * node option; (*current, previous*) |
5828 | 139 |
|
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
140 |
val toplevel = State (NONE, NONE); |
5828 | 141 |
|
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
142 |
fun is_toplevel (State (NONE, _)) = true |
7732 | 143 |
| is_toplevel _ = false; |
144 |
||
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
145 |
fun level (State (NONE, _)) = 0 |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
146 |
| level (State (SOME (Theory _), _)) = 0 |
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
147 |
| level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf) |
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
148 |
| level (State (SOME (SkipProof (d, _)), _)) = d + 1; (*different notion of proof depth!*) |
17076 | 149 |
|
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
150 |
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
|
151 |
| 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
|
152 |
| 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
|
153 |
| str_of_state (State (SOME (Proof _), _)) = "in proof mode" |
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
154 |
| str_of_state (State (SOME (SkipProof _), _)) = "in skipped proof mode"; |
5946
a4600d21b59b
print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents:
5939
diff
changeset
|
155 |
|
a4600d21b59b
print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents:
5939
diff
changeset
|
156 |
|
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
157 |
(* current node *) |
5828 | 158 |
|
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
159 |
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
|
160 |
| node_of (State (SOME node, _)) = node; |
5828 | 161 |
|
18589 | 162 |
fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state)); |
163 |
fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state)); |
|
164 |
||
19063 | 165 |
fun node_case f g state = cases_node f g (node_of state); |
5828 | 166 |
|
30398 | 167 |
fun presentation_context_of state = |
168 |
(case try node_of state of |
|
169 |
SOME (Theory (_, SOME ctxt)) => ctxt |
|
170 |
| SOME node => context_node node |
|
171 |
| NONE => raise UNDEF); |
|
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
172 |
|
30801 | 173 |
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
|
174 |
| previous_context_of (State (_, SOME prev)) = SOME (context_node prev); |
30801 | 175 |
|
21506 | 176 |
val context_of = node_case Context.proof_of Proof.context_of; |
22089 | 177 |
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
|
178 |
val theory_of = node_case Context.theory_of Proof.theory_of; |
18589 | 179 |
val proof_of = node_case (fn _ => raise UNDEF) I; |
17208 | 180 |
|
18589 | 181 |
fun proof_position_of state = |
182 |
(case node_of state of |
|
33390 | 183 |
Proof (prf, _) => Proof_Node.position prf |
18589 | 184 |
| _ => raise UNDEF); |
6664 | 185 |
|
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
186 |
fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy |
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
187 |
| end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos); |
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
188 |
|
5828 | 189 |
|
16815 | 190 |
(* print state *) |
191 |
||
38388 | 192 |
val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I; |
16815 | 193 |
|
23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset
|
194 |
fun print_state_context state = |
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset
|
195 |
(case try node_of state of |
21506 | 196 |
NONE => [] |
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset
|
197 |
| SOME (Theory (gthy, _)) => pretty_context gthy |
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset
|
198 |
| SOME (Proof (_, (_, gthy))) => pretty_context gthy |
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset
|
199 |
| SOME (SkipProof (_, (gthy, _))) => pretty_context gthy) |
23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset
|
200 |
|> Pretty.chunks |> Pretty.writeln; |
16815 | 201 |
|
23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset
|
202 |
fun print_state prf_only state = |
23701 | 203 |
(case try node_of state of |
204 |
NONE => [] |
|
205 |
| SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy |
|
206 |
| SOME (Proof (prf, _)) => |
|
33390 | 207 |
Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf) |
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset
|
208 |
| SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]) |
23701 | 209 |
|> Pretty.markup_chunks Markup.state |> Pretty.writeln; |
16815 | 210 |
|
37858 | 211 |
fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">"); |
212 |
||
16815 | 213 |
|
15668 | 214 |
|
5828 | 215 |
(** toplevel transitions **) |
216 |
||
32738 | 217 |
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
|
218 |
val debug = Runtime.debug; |
32738 | 219 |
val interact = Unsynchronized.ref false; |
16682 | 220 |
val timing = Output.timing; |
32738 | 221 |
val profiling = Unsynchronized.ref 0; |
222 |
val skip_proofs = Unsynchronized.ref false; |
|
16682 | 223 |
|
33604
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
224 |
fun program body = |
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
225 |
(body |
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset
|
226 |
|> Runtime.controlled_execution |
33604
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
227 |
|> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) (); |
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
228 |
|
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
229 |
fun thread interrupts body = |
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
230 |
Thread.fork |
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents:
38888
diff
changeset
|
231 |
(((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
|
232 |
|> Runtime.debugging |
d4220df6fde2
Toplevel.thread provides Isar-style exception output;
wenzelm
parents:
33553
diff
changeset
|
233 |
|> Runtime.toplevel_error |
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39513
diff
changeset
|
234 |
(fn exn => |
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39513
diff
changeset
|
235 |
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
|
236 |
Simple_Thread.attributes interrupts); |
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset
|
237 |
|
5828 | 238 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
239 |
(* node transactions -- maintaining stable checkpoints *) |
7022 | 240 |
|
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset
|
241 |
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
|
242 |
|
6689 | 243 |
local |
244 |
||
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
245 |
fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE) |
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
246 |
| reset_presentation node = node; |
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
247 |
|
26624
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
248 |
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
|
249 |
| is_draft_theory _ = false; |
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
250 |
|
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset
|
251 |
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
|
252 |
|
26624
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
253 |
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
|
254 |
| stale_error some = some; |
16815 | 255 |
|
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
256 |
fun map_theory f (Theory (gthy, ctxt)) = |
33671 | 257 |
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
|
258 |
| map_theory _ node = node; |
6689 | 259 |
|
260 |
in |
|
261 |
||
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
262 |
fun apply_transaction f g node = |
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset
|
263 |
let |
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
264 |
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
|
265 |
val cont_node = reset_presentation node; |
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
266 |
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
|
267 |
fun state_error e nd = (State (SOME nd, SOME node), e); |
6689 | 268 |
|
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset
|
269 |
val (result, err) = |
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset
|
270 |
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
|
271 |
|> Runtime.controlled_execution f |
26624
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
272 |
|> map_theory Theory.checkpoint |
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
273 |
|> state_error NONE |
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
274 |
handle exn => state_error (SOME exn) cont_node; |
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
275 |
|
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
276 |
val (result', err') = |
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
277 |
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
|
278 |
else (result, err); |
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset
|
279 |
in |
26624
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
280 |
(case err' of |
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
281 |
NONE => tap g result' |
26624
770265032999
transaction/init: ensure stable theory (non-draft);
wenzelm
parents:
26621
diff
changeset
|
282 |
| SOME exn => raise FAILURE (result', exn)) |
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset
|
283 |
end; |
6689 | 284 |
|
285 |
end; |
|
286 |
||
287 |
||
288 |
(* primitive transitions *) |
|
289 |
||
5828 | 290 |
datatype trans = |
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
|
291 |
Init of string * (unit -> theory) | (*theory name, init*) |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
292 |
Exit | (*formal exit of theory*) |
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
293 |
Keep of bool -> state -> unit | (*peek at state*) |
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
294 |
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
|
295 |
|
6689 | 296 |
local |
5828 | 297 |
|
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
|
298 |
fun apply_tr _ (Init (_, f)) (State (NONE, _)) = |
33727
e2d5d7f51aa3
init_theory: Runtime.controlled_execution for proper exception trace etc.;
wenzelm
parents:
33725
diff
changeset
|
299 |
State (SOME (Theory (Context.Theory |
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
|
300 |
(Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE) |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
301 |
| apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _)), _)) = |
27603 | 302 |
State (NONE, prev) |
32792 | 303 |
| 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
|
304 |
Runtime.controlled_execution (fn x => tap (f int) x) state |
32792 | 305 |
| apply_tr int (Transaction (f, g)) (State (SOME state, _)) = |
306 |
apply_transaction (fn x => f int x) g state |
|
307 |
| apply_tr _ _ _ = raise UNDEF; |
|
5828 | 308 |
|
32792 | 309 |
fun apply_union _ [] state = raise FAILURE (state, UNDEF) |
310 |
| apply_union int (tr :: trs) state = |
|
311 |
apply_union int trs state |
|
312 |
handle Runtime.UNDEF => apply_tr int tr state |
|
313 |
| FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state |
|
6689 | 314 |
| exn as FAILURE _ => raise exn |
315 |
| exn => raise FAILURE (state, exn); |
|
316 |
||
317 |
in |
|
318 |
||
32792 | 319 |
fun apply_trans int trs state = (apply_union int trs state, NONE) |
15531 | 320 |
handle FAILURE (alt_state, exn) => (alt_state, SOME exn) | exn => (state, SOME exn); |
6689 | 321 |
|
322 |
end; |
|
5828 | 323 |
|
324 |
||
325 |
(* datatype transition *) |
|
326 |
||
327 |
datatype transition = Transition of |
|
26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
328 |
{name: string, (*command name*) |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
329 |
pos: Position.T, (*source position*) |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
330 |
int_only: bool, (*interactive-only*) |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
331 |
print: bool, (*print result state*) |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
332 |
no_timing: bool, (*suppress timing*) |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
333 |
trans: trans list}; (*primitive transitions (union)*) |
5828 | 334 |
|
26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
335 |
fun make_transition (name, pos, int_only, print, no_timing, trans) = |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
336 |
Transition {name = name, pos = pos, int_only = int_only, print = print, no_timing = no_timing, |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
337 |
trans = trans}; |
5828 | 338 |
|
26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
339 |
fun map_transition f (Transition {name, pos, int_only, print, no_timing, trans}) = |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
340 |
make_transition (f (name, pos, int_only, print, no_timing, trans)); |
5828 | 341 |
|
27441 | 342 |
val empty = make_transition ("", Position.none, false, false, false, []); |
5828 | 343 |
|
344 |
||
345 |
(* diagnostics *) |
|
346 |
||
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
347 |
fun init_of (Transition {trans = [Init (name, _)], ...}) = SOME name |
27441 | 348 |
| init_of _ = NONE; |
349 |
||
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset
|
350 |
fun print_of (Transition {print, ...}) = print; |
27427 | 351 |
fun name_of (Transition {name, ...}) = name; |
28105 | 352 |
fun pos_of (Transition {pos, ...}) = pos; |
353 |
fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr); |
|
5828 | 354 |
|
27427 | 355 |
fun command_msg msg tr = msg ^ "command " ^ str_of tr; |
38875
c7a66b584147
tuned messages: discontinued spurious full-stops (messages are occasionally composed unexpectedly);
wenzelm
parents:
38721
diff
changeset
|
356 |
fun at_command tr = command_msg "At " tr; |
5828 | 357 |
|
358 |
fun type_error tr state = |
|
18685 | 359 |
ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); |
5828 | 360 |
|
361 |
||
362 |
(* modify transitions *) |
|
363 |
||
28451
0586b855c2b5
datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents:
28446
diff
changeset
|
364 |
fun name name = map_transition (fn (_, pos, int_only, print, no_timing, trans) => |
0586b855c2b5
datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents:
28446
diff
changeset
|
365 |
(name, pos, int_only, print, no_timing, trans)); |
9010 | 366 |
|
26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
367 |
fun position pos = map_transition (fn (name, _, int_only, print, no_timing, trans) => |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
368 |
(name, pos, int_only, print, no_timing, trans)); |
5828 | 369 |
|
26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
370 |
fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, trans) => |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
371 |
(name, pos, int_only, print, no_timing, trans)); |
14923 | 372 |
|
26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
373 |
val no_timing = map_transition (fn (name, pos, int_only, print, _, trans) => |
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
374 |
(name, pos, int_only, print, true, trans)); |
17363 | 375 |
|
26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
376 |
fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, trans) => |
28451
0586b855c2b5
datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents:
28446
diff
changeset
|
377 |
(name, pos, int_only, print, no_timing, tr :: trans)); |
16607 | 378 |
|
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
379 |
val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, _) => |
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
380 |
(name, pos, int_only, print, no_timing, [])); |
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
381 |
|
28453
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset
|
382 |
fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, trans) => |
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset
|
383 |
(name, pos, int_only, print, no_timing, trans)); |
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset
|
384 |
|
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset
|
385 |
val print = set_print true; |
5828 | 386 |
|
387 |
||
21007 | 388 |
(* basic transitions *) |
5828 | 389 |
|
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
390 |
fun init_theory name f = add_trans (Init (name, 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
|
391 |
|
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
|
392 |
fun modify_init f tr = |
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
|
393 |
(case init_of tr of |
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
|
394 |
SOME name => init_theory name f (reset_trans tr) |
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
|
395 |
| NONE => tr); |
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
|
396 |
|
6689 | 397 |
val exit = add_trans Exit; |
7612 | 398 |
val keep' = add_trans o Keep; |
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
399 |
|
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
400 |
fun present_transaction f g = add_trans (Transaction (f, g)); |
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
401 |
fun transaction f = present_transaction f (K ()); |
5828 | 402 |
|
7612 | 403 |
fun keep f = add_trans (Keep (fn _ => f)); |
5828 | 404 |
fun imperative f = keep (fn _ => f ()); |
405 |
||
27840 | 406 |
fun ignored pos = empty |> name "<ignored>" |> position pos |> imperative I; |
407 |
fun malformed pos msg = |
|
408 |
empty |> name "<malformed>" |> position pos |> imperative (fn () => error msg); |
|
409 |
||
21007 | 410 |
val unknown_theory = imperative (fn () => warning "Unknown theory context"); |
411 |
val unknown_proof = imperative (fn () => warning "Unknown proof context"); |
|
412 |
val unknown_context = imperative (fn () => warning "Unknown context"); |
|
15668 | 413 |
|
21007 | 414 |
|
415 |
(* theory transitions *) |
|
15668 | 416 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
417 |
fun generic_theory f = transaction (fn _ => |
26491 | 418 |
(fn Theory (gthy, _) => Theory (f gthy, NONE) |
419 |
| _ => raise UNDEF)); |
|
420 |
||
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
421 |
fun theory' f = transaction (fn int => |
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
422 |
(fn Theory (Context.Theory thy, _) => |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
423 |
let val thy' = thy |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
424 |
|> Sign.new_group |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
425 |
|> Theory.checkpoint |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
426 |
|> f int |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
427 |
|> Sign.reset_group; |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
428 |
in Theory (Context.Theory thy', NONE) end |
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
429 |
| _ => raise UNDEF)); |
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
430 |
|
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
431 |
fun theory f = theory' (K f); |
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
432 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
433 |
fun begin_local_theory begin f = transaction (fn _ => |
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
434 |
(fn Theory (Context.Theory thy, _) => |
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
435 |
let |
20985 | 436 |
val lthy = f thy; |
21294 | 437 |
val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy); |
438 |
in Theory (gthy, SOME lthy) end |
|
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
439 |
| _ => raise UNDEF)); |
17076 | 440 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
441 |
val end_local_theory = transaction (fn _ => |
21294 | 442 |
(fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy) |
21007 | 443 |
| _ => raise UNDEF)); |
444 |
||
445 |
local |
|
446 |
||
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
447 |
fun local_theory_presentation loc f = present_transaction (fn int => |
21294 | 448 |
(fn Theory (gthy, _) => |
449 |
let |
|
450 |
val finish = loc_finish loc gthy; |
|
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
451 |
val lthy' = loc_begin loc gthy |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
452 |
|> Local_Theory.new_group |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
453 |
|> f int |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
454 |
|> Local_Theory.reset_group; |
21294 | 455 |
in Theory (finish lthy', SOME lthy') end |
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
456 |
| _ => raise UNDEF)); |
15668 | 457 |
|
21007 | 458 |
in |
459 |
||
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
460 |
fun local_theory' loc f = local_theory_presentation loc f (K ()); |
29380 | 461 |
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
|
462 |
fun present_local_theory loc = local_theory_presentation loc (K I); |
18955 | 463 |
|
21007 | 464 |
end; |
465 |
||
466 |
||
467 |
(* proof transitions *) |
|
468 |
||
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
469 |
fun end_proof f = transaction (fn int => |
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset
|
470 |
(fn Proof (prf, (finish, _)) => |
33390 | 471 |
let val state = Proof_Node.current prf in |
21007 | 472 |
if can (Proof.assert_bottom true) state then |
473 |
let |
|
474 |
val ctxt' = f int state; |
|
475 |
val gthy' = finish ctxt'; |
|
476 |
in Theory (gthy', SOME ctxt') end |
|
477 |
else raise UNDEF |
|
478 |
end |
|
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset
|
479 |
| SkipProof (0, (gthy, _)) => Theory (gthy, NONE) |
21007 | 480 |
| _ => raise UNDEF)); |
481 |
||
21294 | 482 |
local |
483 |
||
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
484 |
fun begin_proof init finish = transaction (fn int => |
21294 | 485 |
(fn Theory (gthy, _) => |
486 |
let |
|
24453 | 487 |
val prf = init int gthy; |
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
488 |
val skip = ! skip_proofs; |
40960 | 489 |
val (is_goal, no_skip) = |
490 |
(true, Proof.schematic_goal prf) handle ERROR _ => (false, true); |
|
21294 | 491 |
in |
40960 | 492 |
if is_goal andalso skip andalso no_skip then |
21294 | 493 |
warning "Cannot skip proof of schematic goal statement" |
494 |
else (); |
|
40960 | 495 |
if skip andalso not no_skip then |
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset
|
496 |
SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy)) |
33390 | 497 |
else Proof (Proof_Node.init prf, (finish gthy, gthy)) |
21294 | 498 |
end |
499 |
| _ => raise UNDEF)); |
|
500 |
||
501 |
in |
|
502 |
||
24780
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset
|
503 |
fun local_theory_to_proof' loc f = begin_proof |
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
504 |
(fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy))) |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
505 |
(fn gthy => loc_finish loc gthy o Local_Theory.reset_group); |
24780
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset
|
506 |
|
24453 | 507 |
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f); |
21294 | 508 |
|
509 |
fun theory_to_proof f = begin_proof |
|
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
510 |
(K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy)) | _ => raise UNDEF)) |
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset
|
511 |
(K (Context.Theory o Sign.reset_group o ProofContext.theory_of)); |
21294 | 512 |
|
513 |
end; |
|
514 |
||
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
515 |
val forget_proof = transaction (fn _ => |
21007 | 516 |
(fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) |
517 |
| SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) |
|
518 |
| _ => raise UNDEF)); |
|
519 |
||
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
520 |
val present_proof = present_transaction (fn _ => |
33390 | 521 |
(fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x) |
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset
|
522 |
| skip as SkipProof _ => skip |
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
523 |
| _ => raise UNDEF)); |
21177 | 524 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
525 |
fun proofs' f = transaction (fn int => |
33390 | 526 |
(fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) |
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset
|
527 |
| skip as SkipProof _ => skip |
16815 | 528 |
| _ => raise UNDEF)); |
15668 | 529 |
|
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset
|
530 |
fun proof' f = proofs' (Seq.single oo f); |
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset
|
531 |
val proofs = proofs' o K; |
6689 | 532 |
val proof = proof' o K; |
16815 | 533 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
534 |
fun actual_proof f = transaction (fn _ => |
21007 | 535 |
(fn Proof (prf, x) => Proof (f prf, x) |
20963
a7fd8f05a2be
added type global_theory -- theory or local_theory;
wenzelm
parents:
20928
diff
changeset
|
536 |
| _ => raise UNDEF)); |
16815 | 537 |
|
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
538 |
fun skip_proof f = transaction (fn _ => |
21007 | 539 |
(fn SkipProof (h, x) => SkipProof (f h, x) |
18563 | 540 |
| _ => raise UNDEF)); |
541 |
||
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset
|
542 |
fun skip_proof_to_theory pred = transaction (fn _ => |
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset
|
543 |
(fn SkipProof (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
|
544 |
| _ => raise UNDEF)); |
5828 | 545 |
|
546 |
||
547 |
||
548 |
(** toplevel transactions **) |
|
549 |
||
27427 | 550 |
(* identification *) |
551 |
||
552 |
fun get_id (Transition {pos, ...}) = Position.get_id pos; |
|
553 |
fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr; |
|
554 |
||
555 |
||
25960 | 556 |
(* thread position *) |
25799 | 557 |
|
25960 | 558 |
fun setmp_thread_position (Transition {pos, ...}) f x = |
25819
e6feb08b7f4b
replaced thread_properties by simplified version in position.ML;
wenzelm
parents:
25809
diff
changeset
|
559 |
Position.setmp_thread_data pos f x; |
25799 | 560 |
|
27606 | 561 |
fun status tr m = |
562 |
setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) (); |
|
563 |
||
38876
ec7045139e70
Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
wenzelm
parents:
38875
diff
changeset
|
564 |
fun error_msg tr msg = |
ec7045139e70
Toplevel.run_command: more careful treatment of interrupts stemming from nested multi-exceptions etc.;
wenzelm
parents:
38875
diff
changeset
|
565 |
setmp_thread_position tr (fn () => Output.error_msg msg) (); |
26602
5534b6a6b810
made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset
|
566 |
|
25799 | 567 |
|
28095
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
568 |
(* post-transition hooks *) |
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
569 |
|
37905 | 570 |
local |
571 |
val hooks = Unsynchronized.ref ([]: (transition -> state -> state -> unit) list); |
|
572 |
in |
|
28095
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
573 |
|
32738 | 574 |
fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f)); |
33223 | 575 |
fun get_hooks () = ! hooks; |
28095
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
576 |
|
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
577 |
end; |
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
578 |
|
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
579 |
|
5828 | 580 |
(* apply transitions *) |
581 |
||
6664 | 582 |
local |
583 |
||
32792 | 584 |
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
|
585 |
setmp_thread_position tr (fn state => |
25799 | 586 |
let |
587 |
fun do_timing f x = (warning (command_msg "" tr); timeap f x); |
|
588 |
fun do_profiling f x = profile (! profiling) f x; |
|
589 |
||
26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset
|
590 |
val (result, status) = |
37905 | 591 |
state |> |
592 |
(apply_trans int trans |
|
593 |
|> (! profiling > 0 andalso not no_timing) ? do_profiling |
|
594 |
|> (! 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
|
595 |
|
26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset
|
596 |
val _ = if int andalso not (! quiet) andalso print then print_state false result else (); |
26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset
|
597 |
in (result, Option.map (fn UNDEF => type_error tr state | exn => exn) status) end); |
6664 | 598 |
|
599 |
in |
|
5828 | 600 |
|
26602
5534b6a6b810
made purely value-oriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset
|
601 |
fun transition int tr st = |
28095
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
602 |
let |
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
603 |
val hooks = get_hooks (); |
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset
|
604 |
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
|
605 |
|
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
606 |
val ctxt = try context_of st; |
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
607 |
val res = |
7eaf0813bdc3
added add_hook interface for post-transition hooks;
wenzelm
parents:
27859
diff
changeset
|
608 |
(case app int tr st of |
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset
|
609 |
(_, SOME Runtime.TERMINATE) => NONE |
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset
|
610 |
| (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
|
611 |
| (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
|
612 |
| (st', NONE) => SOME (st', NONE)); |
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset
|
613 |
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
|
614 |
in res end; |
6664 | 615 |
|
616 |
end; |
|
5828 | 617 |
|
618 |
||
28425 | 619 |
(* nested commands *) |
5828 | 620 |
|
28425 | 621 |
fun command tr st = |
27576
7afff36043e6
eliminated internal command history -- superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset
|
622 |
(case transition (! interact) tr st of |
28425 | 623 |
SOME (st', NONE) => st' |
39285 | 624 |
| SOME (_, SOME (exn, info)) => |
625 |
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
|
626 |
| 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
|
627 |
|
29483 | 628 |
fun command_result tr st = |
629 |
let val st' = command tr st |
|
630 |
in (st', st') end; |
|
631 |
||
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
632 |
|
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
633 |
(* excursion of units, consisting of commands with proof *) |
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
634 |
|
33519 | 635 |
structure States = 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
|
636 |
( |
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
|
637 |
type T = state list future option; |
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
|
638 |
fun init _ = NONE; |
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
|
639 |
); |
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
|
640 |
|
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
|
641 |
fun proof_result immediate (tr, proof_trs) st = |
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
642 |
let val st' = command tr st in |
36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
35205
diff
changeset
|
643 |
if immediate orelse |
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
35205
diff
changeset
|
644 |
null proof_trs orelse |
36950 | 645 |
Keyword.is_schematic_goal (name_of tr) orelse |
646 |
exists (Keyword.is_qed_global o name_of) proof_trs orelse |
|
36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
35205
diff
changeset
|
647 |
not (can proof_of st') orelse |
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
35205
diff
changeset
|
648 |
Proof.is_relevant (proof_of st') |
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
649 |
then |
28453
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset
|
650 |
let val (states, st'') = fold_map command_result proof_trs st' |
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
|
651 |
in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end |
28453
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset
|
652 |
else |
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
653 |
let |
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
654 |
val (body_trs, end_tr) = split_last proof_trs; |
28453
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset
|
655 |
val finish = Context.Theory o ProofContext.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
|
656 |
|
29386 | 657 |
val future_proof = Proof.global_future_proof |
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
|
658 |
(fn prf => |
32062
457f5bcd3d76
Proof.future_proof: declare all assumptions as well;
wenzelm
parents:
32058
diff
changeset
|
659 |
Future.fork_pri ~1 (fn () => |
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset
|
660 |
let val (states, result_state) = |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
661 |
(case st' of State (SOME (Proof (_, (_, orig_gthy))), prev) |
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
662 |
=> State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev)) |
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
|
663 |
|> fold_map command_result body_trs |
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
|
664 |
||> command (end_tr |> set_print false); |
30398 | 665 |
in (states, presentation_context_of result_state) end)) |
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
|
666 |
#> (fn (states, ctxt) => States.put (SOME states) ctxt); |
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
|
667 |
|
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
|
668 |
val st'' = st' |> command (end_tr |> reset_trans |> end_proof (K future_proof)); |
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
|
669 |
|
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
|
670 |
val states = |
30398 | 671 |
(case States.get (presentation_context_of st'') of |
37852
a902f158b4fc
eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
wenzelm
parents:
37711
diff
changeset
|
672 |
NONE => raise Fail ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr)) |
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
|
673 |
| SOME states => states); |
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
|
674 |
val result = Lazy.lazy |
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
|
675 |
(fn () => (tr, st') :: (body_trs ~~ Future.join states) @ [(end_tr, st'')]); |
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
|
676 |
|
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
|
677 |
in (result, st'') end |
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
678 |
end; |
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
679 |
|
29068 | 680 |
fun excursion input = |
28425 | 681 |
let |
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset
|
682 |
val end_pos = if null input then error "No input" else pos_of (fst (List.last input)); |
29448
34b9652b2f45
added Goal.future_enabled abstraction -- now also checks that this is already
wenzelm
parents:
29435
diff
changeset
|
683 |
val immediate = not (Goal.future_enabled ()); |
29427
7ba952481e29
excursion: commit_exit internally -- checkpoints are fully persistent now;
wenzelm
parents:
29386
diff
changeset
|
684 |
val (results, end_state) = fold_map (proof_result immediate) input toplevel; |
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
685 |
val thy = end_theory end_pos end_state; |
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset
|
686 |
in (Lazy.lazy (fn () => maps Lazy.force results), thy) end; |
7062 | 687 |
|
6664 | 688 |
end; |