author  wenzelm 
Tue, 09 Apr 2013 15:29:25 +0200  
changeset 51658  21c10672633b 
parent 51605  eca8acb42e4a 
child 51661  92e58b76dbb1 
permissions  rwrr 
5828  1 
(* Title: Pure/Isar/toplevel.ML 
2 
Author: Markus Wenzel, TU Muenchen 

3 

26602
5534b6a6b810
made purely valueoriented, 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 valueoriented, 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 Isarstyle 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 
44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

45 
val init_theory: (unit > theory) > transition > transition 
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

46 
val is_init: transition > bool 
44186
806f0ec1a43d
simplified Toplevel.init_theory: discontinued special master argument;
wenzelm
parents:
44185
diff
changeset

47 
val modify_init: (unit > theory) > transition > transition 
6689  48 
val exit: transition > transition 
5828  49 
val keep: (state > unit) > transition > transition 
7612  50 
val keep': (bool > state > unit) > transition > transition 
5828  51 
val imperative: (unit > unit) > transition > transition 
27840  52 
val ignored: Position.T > transition 
51268
fcc4b89a600d
simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
wenzelm
parents:
51241
diff
changeset

53 
val is_ignored: transition > bool 
27840  54 
val malformed: Position.T > string > transition 
48772  55 
val is_malformed: transition > bool 
26491  56 
val generic_theory: (generic_theory > generic_theory) > transition > transition 
7612  57 
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

58 
val theory: (theory > theory) > transition > transition 
20985  59 
val begin_local_theory: bool > (theory > local_theory) > transition > transition 
21007  60 
val end_local_theory: transition > transition 
47069  61 
val open_target: (generic_theory > local_theory) > transition > transition 
62 
val close_target: transition > transition 

45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset

63 
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

64 
transition > transition 
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset

65 
val local_theory: (xstring * Position.T) option > (local_theory > local_theory) > 
29380  66 
transition > transition 
45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset

67 
val present_local_theory: (xstring * Position.T) option > (state > unit) > 
24453  68 
transition > transition 
45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset

69 
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

70 
(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

71 
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

72 
(local_theory > Proof.state) > transition > transition 
17363  73 
val theory_to_proof: (theory > Proof.state) > transition > transition 
21007  74 
val end_proof: (bool > Proof.state > Proof.context) > transition > transition 
75 
val forget_proof: transition > transition 

30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

76 
val present_proof: (state > unit) > transition > transition 
49863
b5fb6e7f8d81
more informative errors for 'proof' and 'apply' steps;
wenzelm
parents:
49062
diff
changeset

77 
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

78 
val proof': (bool > Proof.state > Proof.state) > transition > transition 
49863
b5fb6e7f8d81
more informative errors for 'proof' and 'apply' steps;
wenzelm
parents:
49062
diff
changeset

79 
val proofs: (Proof.state > Proof.state Seq.result Seq.seq) > transition > transition 
21177  80 
val proof: (Proof.state > Proof.state) > transition > transition 
33390  81 
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

82 
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

83 
val skip_proof_to_theory: (int > bool) > transition > transition 
27427  84 
val get_id: transition > string option 
85 
val put_id: string > transition > transition 

9512  86 
val unknown_theory: transition > transition 
87 
val unknown_proof: transition > transition 

88 
val unknown_context: transition > transition 

28425  89 
val setmp_thread_position: transition > ('a > 'b) > 'a > 'b 
27606  90 
val status: transition > Markup.T > unit 
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset

91 
val add_hook: (transition > state > state > unit) > unit 
51228  92 
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

93 
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

94 
val put_timing: Time.time option > transition > transition 
26602
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

95 
val transition: bool > transition > state > (state * (exn * string) option) option 
51323  96 
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

97 
val command_exception: bool > transition > state > state 
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

98 
type result 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

99 
val join_results: result > (transition * state) list 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

100 
val element_result: transition Thy_Syntax.element > state > result * state 
5828  101 
end; 
102 

6965  103 
structure Toplevel: TOPLEVEL = 
5828  104 
struct 
105 

106 
(** toplevel state **) 

107 

31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset

108 
exception UNDEF = Runtime.UNDEF; 
19063  109 

110 

21294  111 
(* local theory wrappers *) 
5828  112 

38350
480b2de9927c
renamed Theory_Target to the more appropriate Named_Target
haftmann
parents:
38236
diff
changeset

113 
val loc_init = Named_Target.context_cmd; 
47069  114 
val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global; 
21294  115 

47274  116 
fun loc_begin loc (Context.Theory thy) = 
117 
(Context.Theory o loc_exit, loc_init (the_default ("", Position.none) loc) thy) 

118 
 loc_begin NONE (Context.Proof lthy) = 

119 
(Context.Proof o Local_Theory.restore, lthy) 

120 
 loc_begin (SOME loc) (Context.Proof lthy) = 

121 
(Context.Proof o Named_Target.reinit lthy, loc_init loc (loc_exit lthy)); 

21294  122 

123 

21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

124 
(* datatype node *) 
21294  125 

5828  126 
datatype node = 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

127 
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

128 
(*theory with presentation context*)  
33390  129 
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

130 
(*proof node, finish, original theory*)  
51555  131 
Skipped_Proof of int * (generic_theory * generic_theory); 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

132 
(*proof depth, resulting theory, original theory*) 
5828  133 

20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

134 
val theory_node = fn Theory (gthy, _) => SOME gthy  _ => NONE; 
18589  135 
val proof_node = fn Proof (prf, _) => SOME prf  _ => NONE; 
51555  136 
val skipped_proof_node = fn Skipped_Proof _ => true  _ => false; 
18589  137 

20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

138 
fun cases_node f _ (Theory (gthy, _)) = f gthy 
33390  139 
 cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf) 
51555  140 
 cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy; 
19063  141 

29066  142 
val context_node = cases_node Context.proof_of Proof.context_of; 
143 

21958
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

144 

9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

145 
(* datatype state *) 
9dfd1ca4c0a0
refined notion of empty toplevel, admits undo of 'end';
wenzelm
parents:
21861
diff
changeset

146 

37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

147 
datatype state = State of node option * node option; (*current, previous*) 
5828  148 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

149 
val toplevel = State (NONE, NONE); 
5828  150 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

151 
fun is_toplevel (State (NONE, _)) = true 
7732  152 
 is_toplevel _ = false; 
153 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

154 
fun level (State (NONE, _)) = 0 
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

155 
 level (State (SOME (Theory _), _)) = 0 
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

156 
 level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf) 
51555  157 
 level (State (SOME (Skipped_Proof (d, _)), _)) = d + 1; (*different notion of proof depth!*) 
17076  158 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

159 
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

160 
 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

161 
 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

162 
 str_of_state (State (SOME (Proof _), _)) = "in proof mode" 
51555  163 
 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

164 

a4600d21b59b
print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents:
5939
diff
changeset

165 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

166 
(* current node *) 
5828  167 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

168 
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

169 
 node_of (State (SOME node, _)) = node; 
5828  170 

18589  171 
fun is_theory state = not (is_toplevel state) andalso is_some (theory_node (node_of state)); 
172 
fun is_proof state = not (is_toplevel state) andalso is_some (proof_node (node_of state)); 

51555  173 
fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state); 
18589  174 

19063  175 
fun node_case f g state = cases_node f g (node_of state); 
5828  176 

30398  177 
fun presentation_context_of state = 
178 
(case try node_of state of 

179 
SOME (Theory (_, SOME ctxt)) => ctxt 

180 
 SOME node => context_node node 

181 
 NONE => raise UNDEF); 

30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

182 

30801  183 
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

184 
 previous_context_of (State (_, SOME prev)) = SOME (context_node prev); 
30801  185 

21506  186 
val context_of = node_case Context.proof_of Proof.context_of; 
22089  187 
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

188 
val theory_of = node_case Context.theory_of Proof.theory_of; 
18589  189 
val proof_of = node_case (fn _ => raise UNDEF) I; 
17208  190 

18589  191 
fun proof_position_of state = 
192 
(case node_of state of 

33390  193 
Proof (prf, _) => Proof_Node.position prf 
18589  194 
 _ => raise UNDEF); 
6664  195 

43667
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

196 
fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = thy 
48992  197 
 end_theory pos (State (NONE, _)) = error ("Bad theory" ^ Position.here pos) 
198 
 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

199 

5828  200 

16815  201 
(* print state *) 
202 

38388  203 
val pretty_context = Local_Theory.pretty o Context.cases (Named_Target.theory_init) I; 
16815  204 

23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

205 
fun print_state_context state = 
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

206 
(case try node_of state of 
21506  207 
NONE => [] 
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

208 
 SOME (Theory (gthy, _)) => pretty_context gthy 
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

209 
 SOME (Proof (_, (_, gthy))) => pretty_context gthy 
51555  210 
 SOME (Skipped_Proof (_, (gthy, _))) => pretty_context gthy) 
23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

211 
> Pretty.chunks > Pretty.writeln; 
16815  212 

23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

213 
fun print_state prf_only state = 
23701  214 
(case try node_of state of 
215 
NONE => [] 

216 
 SOME (Theory (gthy, _)) => if prf_only then [] else pretty_context gthy 

217 
 SOME (Proof (prf, _)) => 

33390  218 
Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf) 
51555  219 
 SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]) 
50201
c26369c9eda6
Isabellespecific implementation of quasiabstract markup elements  back to module arrangement before d83797ef0d2d;
wenzelm
parents:
49863
diff
changeset

220 
> Pretty.markup_chunks Markup.state > Pretty.writeln; 
16815  221 

37858  222 
fun pretty_abstract state = Pretty.str ("<Isar " ^ str_of_state state ^ ">"); 
223 

16815  224 

15668  225 

5828  226 
(** toplevel transitions **) 
227 

32738  228 
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

229 
val debug = Runtime.debug; 
32738  230 
val interact = Unsynchronized.ref false; 
42012
2c3fe3cbebae
structure Timing: covers former start_timing/end_timing and Output.timeit etc;
wenzelm
parents:
41703
diff
changeset

231 
val timing = Unsynchronized.ref false; 
32738  232 
val profiling = Unsynchronized.ref 0; 
16682  233 

33604
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

234 
fun program body = 
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

235 
(body 
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset

236 
> Runtime.controlled_execution 
33604
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

237 
> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) (); 
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

238 

d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

239 
fun thread interrupts body = 
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

240 
Thread.fork 
39232
69c6d3e87660
more abstract treatment of interrupts in structure Exn  hardly ever need to mention Interrupt literally;
wenzelm
parents:
38888
diff
changeset

241 
(((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn) 
33604
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

242 
> Runtime.debugging 
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

243 
> Runtime.toplevel_error 
40132
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39513
diff
changeset

244 
(fn exn => 
7ee65dbffa31
renamed Output.priority to Output.urgent_message to emphasize its special role more clearly;
wenzelm
parents:
39513
diff
changeset

245 
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

246 
Simple_Thread.attributes interrupts); 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

247 

5828  248 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

249 
(* node transactions  maintaining stable checkpoints *) 
7022  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 
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

252 

6689  253 
local 
254 

30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

255 
fun reset_presentation (Theory (gthy, _)) = Theory (gthy, NONE) 
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

256 
 reset_presentation node = node; 
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

257 

26624
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

258 
fun is_draft_theory (Theory (gthy, _)) = Context.is_draft (Context.theory_of gthy) 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

259 
 is_draft_theory _ = false; 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

260 

31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset

261 
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

262 

26624
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

263 
fun stale_error NONE = SOME (ERROR "Stale theory encountered after successful execution!") 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

264 
 stale_error some = some; 
16815  265 

27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

266 
fun map_theory f (Theory (gthy, ctxt)) = 
33671  267 
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

268 
 map_theory _ node = node; 
6689  269 

270 
in 

271 

37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

272 
fun apply_transaction f g node = 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

273 
let 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

274 
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

275 
val cont_node = reset_presentation node; 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

276 
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

277 
fun state_error e nd = (State (SOME nd, SOME node), e); 
6689  278 

20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

279 
val (result, err) = 
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

280 
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

281 
> Runtime.controlled_execution f 
26624
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

282 
> map_theory Theory.checkpoint 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

283 
> state_error NONE 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

284 
handle exn => state_error (SOME exn) cont_node; 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

285 

770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

286 
val (result', err') = 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

287 
if is_stale result then state_error (stale_error err) back_node 
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

288 
else (result, err); 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

289 
in 
26624
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

290 
(case err' of 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

291 
NONE => tap g result' 
26624
770265032999
transaction/init: ensure stable theory (nondraft);
wenzelm
parents:
26621
diff
changeset

292 
 SOME exn => raise FAILURE (result', exn)) 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

293 
end; 
6689  294 

43667
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

295 
val exit_transaction = 
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

296 
apply_transaction 
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

297 
(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 HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

298 
 node => node) (K ()) 
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

299 
#> (fn State (node', _) => State (NONE, node')); 
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

300 

6689  301 
end; 
302 

303 

304 
(* primitive transitions *) 

305 

5828  306 
datatype trans = 
44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

307 
Init of unit > theory  (*init theory*) 
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

308 
Exit  (*formal exit of theory*) 
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

309 
Keep of bool > state > unit  (*peek at state*) 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

310 
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

311 

6689  312 
local 
5828  313 

44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

314 
fun apply_tr _ (Init f) (State (NONE, _)) = 
33727
e2d5d7f51aa3
init_theory: Runtime.controlled_execution for proper exception trace etc.;
wenzelm
parents:
33725
diff
changeset

315 
State (SOME (Theory (Context.Theory 
44186
806f0ec1a43d
simplified Toplevel.init_theory: discontinued special master argument;
wenzelm
parents:
44185
diff
changeset

316 
(Theory.checkpoint (Runtime.controlled_execution f ())), NONE)), NONE) 
43667
6d73cceb1503
explicit exit_transaction with Theory.end_theory (which could include sanity checks as in HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

317 
 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 HOLSPARK for example);
wenzelm
parents:
43665
diff
changeset

318 
exit_transaction state 
32792  319 
 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

320 
Runtime.controlled_execution (fn x => tap (f int) x) state 
32792  321 
 apply_tr int (Transaction (f, g)) (State (SOME state, _)) = 
322 
apply_transaction (fn x => f int x) g state 

323 
 apply_tr _ _ _ = raise UNDEF; 

5828  324 

32792  325 
fun apply_union _ [] state = raise FAILURE (state, UNDEF) 
326 
 apply_union int (tr :: trs) state = 

327 
apply_union int trs state 

328 
handle Runtime.UNDEF => apply_tr int tr state 

329 
 FAILURE (alt_state, UNDEF) => apply_tr int tr alt_state 

6689  330 
 exn as FAILURE _ => raise exn 
331 
 exn => raise FAILURE (state, exn); 

332 

333 
in 

334 

32792  335 
fun apply_trans int trs state = (apply_union int trs state, NONE) 
15531  336 
handle FAILURE (alt_state, exn) => (alt_state, SOME exn)  exn => (state, SOME exn); 
6689  337 

338 
end; 

5828  339 

340 

341 
(* datatype transition *) 

342 

343 
datatype transition = Transition of 

26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

344 
{name: string, (*command name*) 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

345 
pos: Position.T, (*source position*) 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

346 
int_only: bool, (*interactiveonly*) 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

347 
print: bool, (*print result state*) 
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

348 
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

349 
trans: trans list}; (*primitive transitions (union)*) 
5828  350 

51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

351 
fun make_transition (name, pos, int_only, print, timing, trans) = 
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset

352 
Transition {name = name, pos = pos, int_only = int_only, print = print, 
51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

353 
timing = timing, trans = trans}; 
5828  354 

51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

355 
fun map_transition f (Transition {name, pos, int_only, print, timing, trans}) = 
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

356 
make_transition (f (name, pos, int_only, print, timing, trans)); 
5828  357 

51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

358 
val empty = make_transition ("", Position.none, false, false, NONE, []); 
5828  359 

360 

361 
(* diagnostics *) 

362 

38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset

363 
fun print_of (Transition {print, ...}) = print; 
27427  364 
fun name_of (Transition {name, ...}) = name; 
28105  365 
fun pos_of (Transition {pos, ...}) = pos; 
5828  366 

48993  367 
fun command_msg msg tr = msg ^ "command " ^ quote (name_of tr) ^ Position.here (pos_of tr); 
38875
c7a66b584147
tuned messages: discontinued spurious fullstops (messages are occasionally composed unexpectedly);
wenzelm
parents:
38721
diff
changeset

368 
fun at_command tr = command_msg "At " tr; 
5828  369 

370 
fun type_error tr state = 

18685  371 
ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); 
5828  372 

373 

374 
(* modify transitions *) 

375 

51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

376 
fun name name = map_transition (fn (_, pos, int_only, print, timing, trans) => 
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

377 
(name, pos, int_only, print, timing, trans)); 
9010  378 

51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

379 
fun position pos = map_transition (fn (name, _, int_only, print, timing, trans) => 
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

380 
(name, pos, int_only, print, timing, trans)); 
5828  381 

51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

382 
fun interactive int_only = map_transition (fn (name, pos, _, print, timing, trans) => 
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

383 
(name, pos, int_only, print, timing, trans)); 
14923  384 

51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

385 
fun add_trans tr = map_transition (fn (name, pos, int_only, print, timing, trans) => 
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

386 
(name, pos, int_only, print, timing, tr :: trans)); 
16607  387 

51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

388 
val reset_trans = map_transition (fn (name, pos, int_only, print, timing, _) => 
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

389 
(name, pos, int_only, print, timing, [])); 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

390 

51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

391 
fun set_print print = map_transition (fn (name, pos, int_only, _, timing, trans) => 
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

392 
(name, pos, int_only, print, 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

393 

06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

394 
val print = set_print true; 
5828  395 

396 

21007  397 
(* basic transitions *) 
5828  398 

44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

399 
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, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37953
diff
changeset

400 

44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

401 
fun is_init (Transition {trans = [Init _], ...}) = true 
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

402 
 is_init _ = false; 
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

403 

88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

404 
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, nonoptional master dependency, do not store text in deps;
wenzelm
parents:
37953
diff
changeset

405 

6689  406 
val exit = add_trans Exit; 
7612  407 
val keep' = add_trans o Keep; 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

408 

e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

409 
fun present_transaction f g = add_trans (Transaction (f, g)); 
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

410 
fun transaction f = present_transaction f (K ()); 
5828  411 

7612  412 
fun keep f = add_trans (Keep (fn _ => f)); 
5828  413 
fun imperative f = keep (fn _ => f ()); 
414 

27840  415 
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

416 
fun is_ignored tr = name_of tr = "<ignored>"; 
48772  417 

418 
val malformed_name = "<malformed>"; 

27840  419 
fun malformed pos msg = 
48772  420 
empty > name malformed_name > position pos > imperative (fn () => error msg); 
421 
fun is_malformed tr = name_of tr = malformed_name; 

27840  422 

21007  423 
val unknown_theory = imperative (fn () => warning "Unknown theory context"); 
424 
val unknown_proof = imperative (fn () => warning "Unknown proof context"); 

425 
val unknown_context = imperative (fn () => warning "Unknown context"); 

15668  426 

21007  427 

49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

428 
(* theory transitions *) 
44304
7ee000ce5390
maintain recent future proofs at transaction boundaries;
wenzelm
parents:
44270
diff
changeset

429 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

430 
fun generic_theory f = transaction (fn _ => 
26491  431 
(fn Theory (gthy, _) => Theory (f gthy, NONE) 
432 
 _ => raise UNDEF)); 

433 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

434 
fun theory' f = transaction (fn int => 
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

435 
(fn Theory (Context.Theory thy, _) => 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

436 
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

437 
> Sign.new_group 
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

438 
> Theory.checkpoint 
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

439 
> f int 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

440 
> Sign.reset_group; 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

441 
in Theory (Context.Theory thy', NONE) end 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

442 
 _ => raise UNDEF)); 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

443 

a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

444 
fun theory f = theory' (K f); 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

445 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

446 
fun begin_local_theory begin f = transaction (fn _ => 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

447 
(fn Theory (Context.Theory thy, _) => 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

448 
let 
20985  449 
val lthy = f thy; 
21294  450 
val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy); 
451 
in Theory (gthy, SOME lthy) end 

20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

452 
 _ => raise UNDEF)); 
17076  453 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

454 
val end_local_theory = transaction (fn _ => 
21294  455 
(fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy) 
21007  456 
 _ => raise UNDEF)); 
457 

47069  458 
fun open_target f = transaction (fn _ => 
459 
(fn Theory (gthy, _) => 

460 
let val lthy = f gthy 

461 
in Theory (Context.Proof lthy, SOME lthy) end 

462 
 _ => raise UNDEF)); 

463 

464 
val close_target = transaction (fn _ => 

465 
(fn Theory (Context.Proof lthy, _) => 

466 
(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

467 
SOME ctxt' => 
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50201
diff
changeset

468 
let 
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50201
diff
changeset

469 
val gthy' = 
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50201
diff
changeset

470 
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

471 
then Context.Proof ctxt' 
5165d7e6d3b9
more precise Local_Theory.level: 1 really means main target and >= 2 nested context;
wenzelm
parents:
50201
diff
changeset

472 
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

473 
in Theory (gthy', SOME lthy) end 
47069  474 
 NONE => raise UNDEF) 
475 
 _ => raise UNDEF)); 

476 

477 

21007  478 
local 
479 

30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

480 
fun local_theory_presentation loc f = present_transaction (fn int => 
21294  481 
(fn Theory (gthy, _) => 
482 
let 

49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49042
diff
changeset

483 
val (finish, lthy) = loc_begin loc gthy; 
47274  484 
val lthy' = lthy 
49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

485 
> Local_Theory.new_group 
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

486 
> f int 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

487 
> Local_Theory.reset_group; 
21294  488 
in Theory (finish lthy', SOME lthy') end 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

489 
 _ => raise UNDEF)); 
15668  490 

21007  491 
in 
492 

30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

493 
fun local_theory' loc f = local_theory_presentation loc f (K ()); 
29380  494 
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

495 
fun present_local_theory loc = local_theory_presentation loc (K I); 
18955  496 

21007  497 
end; 
498 

499 

500 
(* proof transitions *) 

501 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

502 
fun end_proof f = transaction (fn int => 
24795
6f5cb7885fd7
print_state_context: local theory context, not proof context;
wenzelm
parents:
24780
diff
changeset

503 
(fn Proof (prf, (finish, _)) => 
33390  504 
let val state = Proof_Node.current prf in 
21007  505 
if can (Proof.assert_bottom true) state then 
506 
let 

507 
val ctxt' = f int state; 

508 
val gthy' = finish ctxt'; 

509 
in Theory (gthy', SOME ctxt') end 

510 
else raise UNDEF 

511 
end 

51555  512 
 Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE) 
21007  513 
 _ => raise UNDEF)); 
514 

21294  515 
local 
516 

47274  517 
fun begin_proof init = transaction (fn int => 
21294  518 
(fn Theory (gthy, _) => 
519 
let 

47274  520 
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

521 
val skip = ! Goal.skip_proofs; 
40960  522 
val (is_goal, no_skip) = 
523 
(true, Proof.schematic_goal prf) handle ERROR _ => (false, true); 

47274  524 
val _ = 
525 
if is_goal andalso skip andalso no_skip then 

526 
warning "Cannot skip proof of schematic goal statement" 

527 
else (); 

21294  528 
in 
40960  529 
if skip andalso not no_skip then 
51555  530 
Skipped_Proof (0, (finish (Proof.global_skip_proof true prf), gthy)) 
47274  531 
else Proof (Proof_Node.init prf, (finish, gthy)) 
21294  532 
end 
533 
 _ => raise UNDEF)); 

534 

535 
in 

536 

24780
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset

537 
fun local_theory_to_proof' loc f = begin_proof 
47274  538 
(fn int => fn gthy => 
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49042
diff
changeset

539 
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

540 
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

541 

24453  542 
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f); 
21294  543 

544 
fun theory_to_proof f = begin_proof 

47274  545 
(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

546 
(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

547 
(case gthy of 
49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

548 
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

549 
 _ => raise UNDEF))); 
21294  550 

551 
end; 

552 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

553 
val forget_proof = transaction (fn _ => 
21007  554 
(fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 
51555  555 
 Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 
21007  556 
 _ => raise UNDEF)); 
557 

30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

558 
val present_proof = present_transaction (fn _ => 
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49042
diff
changeset

559 
(fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x) 
51555  560 
 skip as Skipped_Proof _ => skip 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

561 
 _ => raise UNDEF)); 
21177  562 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

563 
fun proofs' f = transaction (fn int => 
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49042
diff
changeset

564 
(fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) 
51555  565 
 skip as Skipped_Proof _ => skip 
16815  566 
 _ => raise UNDEF)); 
15668  567 

49863
b5fb6e7f8d81
more informative errors for 'proof' and 'apply' steps;
wenzelm
parents:
49062
diff
changeset

568 
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

569 
val proofs = proofs' o K; 
6689  570 
val proof = proof' o K; 
16815  571 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

572 
fun actual_proof f = transaction (fn _ => 
21007  573 
(fn Proof (prf, x) => Proof (f prf, x) 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

574 
 _ => raise UNDEF)); 
16815  575 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

576 
fun skip_proof f = transaction (fn _ => 
51555  577 
(fn Skipped_Proof (h, x) => Skipped_Proof (f h, x) 
18563  578 
 _ => raise UNDEF)); 
579 

27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

580 
fun skip_proof_to_theory pred = transaction (fn _ => 
51555  581 
(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

582 
 _ => raise UNDEF)); 
5828  583 

584 

585 

586 
(** toplevel transactions **) 

587 

27427  588 
(* identification *) 
589 

590 
fun get_id (Transition {pos, ...}) = Position.get_id pos; 

591 
fun put_id id (tr as Transition {pos, ...}) = position (Position.put_id id pos) tr; 

592 

593 

51228  594 
(* approximative identification within source file *) 
595 

596 
fun approximative_id tr = 

597 
let 

598 
val name = name_of tr; 

599 
val pos = pos_of tr; 

600 
in 

601 
(case (Position.file_of pos, Position.offset_of pos) of 

602 
(SOME file, SOME offset) => SOME {file = file, offset = offset, name = name} 

603 
 _ => NONE) 

604 
end; 

605 

606 

25960  607 
(* thread position *) 
25799  608 

25960  609 
fun setmp_thread_position (Transition {pos, ...}) f x = 
25819
e6feb08b7f4b
replaced thread_properties by simplified version in position.ML;
wenzelm
parents:
25809
diff
changeset

610 
Position.setmp_thread_data pos f x; 
25799  611 

27606  612 
fun status tr m = 
43665  613 
setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) (); 
27606  614 

25799  615 

28095
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

616 
(* posttransition hooks *) 
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

617 

37905  618 
local 
619 
val hooks = Unsynchronized.ref ([]: (transition > state > state > unit) list); 

620 
in 

28095
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

621 

32738  622 
fun add_hook f = CRITICAL (fn () => Unsynchronized.change hooks (cons f)); 
33223  623 
fun get_hooks () = ! hooks; 
28095
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

624 

7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

625 
end; 
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

626 

7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

627 

5828  628 
(* apply transitions *) 
629 

51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset

630 
fun get_timing (Transition {timing, ...}) = timing; 
51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

631 
fun put_timing timing = map_transition (fn (name, pos, int_only, print, _, trans) => 
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

632 
(name, pos, int_only, print, timing, trans)); 
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset

633 

6664  634 
local 
635 

51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

636 
fun app int (tr as Transition {trans, print, ...}) = 
25819
e6feb08b7f4b
replaced thread_properties by simplified version in position.ML;
wenzelm
parents:
25809
diff
changeset

637 
setmp_thread_position tr (fn state => 
25799  638 
let 
51595  639 
val timing_start = Timing.start (); 
25799  640 

51595  641 
val (result, opt_err) = 
51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

642 
state > (apply_trans int trans > ! profiling > 0 ? profile (! profiling)); 
26621
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

643 
val _ = if int andalso not (! quiet) andalso print then print_state false result else (); 
51216  644 

51595  645 
val timing_result = Timing.result timing_start; 
646 

647 
val _ = 

51658
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

648 
if Timing.is_relevant timing_result andalso (! profiling > 0 orelse ! timing) 
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

649 
andalso not (Keyword.is_control (name_of tr)) 
21c10672633b
discontinued Toplevel.no_timing complication  also recovers timing of diagnostic commands, e.g. 'find_theorems';
wenzelm
parents:
51605
diff
changeset

650 
then tracing (command_msg "" tr ^ ": " ^ Timing.message timing_result) 
51595  651 
else (); 
652 
val _ = 

653 
if Timing.is_relevant timing_result 

654 
then status tr (Markup.timing timing_result) 

655 
else (); 

656 
val _ = 

657 
(case approximative_id tr of 

658 
SOME id => 

659 
(Output.protocol_message 

660 
(Markup.command_timing :: 

661 
Markup.command_timing_properties id (#elapsed timing_result)) "" 

662 
handle Fail _ => ()) 

663 
 NONE => ()); 

664 
in 

665 
(result, Option.map (fn UNDEF => type_error tr state  exn => exn) opt_err) 

666 
end); 

6664  667 

668 
in 

5828  669 

26602
5534b6a6b810
made purely valueoriented, 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 posttransition hooks;
wenzelm
parents:
27859
diff
changeset

671 
let 
7eaf0813bdc3
added add_hook interface for posttransition 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 posttransition hooks;
wenzelm
parents:
27859
diff
changeset

674 

7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

675 
val ctxt = try context_of st; 
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

676 
val res = 
7eaf0813bdc3
added add_hook interface for posttransition 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 posttransition 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 subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

708 
datatype result = 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

709 
Result of transition * state  
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

710 
Result_List of result list  
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

711 
Result_Future of result future; 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

712 

8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

713 
fun join_results (Result x) = [x] 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, 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 subproofs, 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 subproofs, 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 lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

720 
( 
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

721 
type T = result; 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, 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 lowlevel 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 lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

725 

51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, 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 subproofs, 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 

51605
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

759 
(Goal.fork_params 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

760 
{name = "Toplevel.diag", pos = pos_of tr, 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

761 
pri = priority (timing_estimate true (Thy_Syntax.atom tr))} 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

762 
(fn () => command tr st); st) 
51323  763 
else command tr st; 
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

764 
in (Result (tr, st'), st') end; 
51323  765 

766 
in 

767 

51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

768 
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

769 
 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

770 
let 
51324  771 
val (head_result, st') = atom_result head_tr st; 
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

772 
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

773 
val estimate = timing_estimate false elem; 
51324  774 
in 
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

775 
if not (proof_future_enabled estimate st') 
51324  776 
then 
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

777 
let 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

778 
val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr]; 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

779 
val (proof_results, st'') = fold_map atom_result proof_trs st'; 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

780 
in (Result_List (head_result :: proof_results), st'') end 
51324  781 
else 
782 
let 

783 
val finish = Context.Theory o Proof_Context.theory_of; 

28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

784 

51605
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

785 
val future_proof = 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

786 
Proof.future_proof (fn state => 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

787 
Goal.fork_params 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

788 
{name = "Toplevel.future_proof", pos = pos_of head_tr, pri = priority estimate} 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

789 
(fn () => 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

790 
let 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

791 
val State (SOME (Proof (prf, (_, orig_gthy))), prev) = st'; 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

792 
val prf' = Proof_Node.apply (K state) prf; 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

793 
val (result, result_state) = 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

794 
State (SOME (Proof (prf', (finish, orig_gthy))), prev) 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

795 
> fold_map element_result body_elems > command end_tr; 
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

796 
in (Result_List result, presentation_context_of result_state) end)) 
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, 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 subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

798 

8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

799 
val forked_proof = 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

800 
proof (future_proof #> 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, 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 subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

802 
end_proof (fn _ => future_proof #> 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, 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 lowlevel 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 subproofs, 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 subproofs, 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 subproofs, 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; 