author  wenzelm 
Fri, 18 Mar 2016 16:26:35 +0100  
changeset 62663  bea354f6ff21 
parent 62505  9e2a65912111 
child 62819  d3ff367a16a0 
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 
56893  25 
val pretty_context: state > Pretty.T list 
56887
1ca814da47ae
clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;
wenzelm
parents:
56867
diff
changeset

26 
val pretty_state: state > Pretty.T list 
61208  27 
val string_of_state: state > string 
37858  28 
val pretty_abstract: state > Pretty.T 
16682  29 
type transition 
5828  30 
val empty: transition 
27427  31 
val name_of: transition > string 
28105  32 
val pos_of: transition > Position.T 
60076  33 
val type_error: transition > string 
5828  34 
val name: string > transition > transition 
35 
val position: Position.T > transition > transition 

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

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

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

38 
val modify_init: (unit > theory) > transition > transition 
6689  39 
val exit: transition > transition 
5828  40 
val keep: (state > unit) > transition > transition 
7612  41 
val keep': (bool > state > unit) > transition > transition 
60190
906de96ba68a
allow diagnostic proof commands with skip_proofs;
wenzelm
parents:
60189
diff
changeset

42 
val keep_proof: (state > unit) > transition > transition 
27840  43 
val ignored: Position.T > transition 
51268
fcc4b89a600d
simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
wenzelm
parents:
51241
diff
changeset

44 
val is_ignored: transition > bool 
27840  45 
val malformed: Position.T > string > transition 
26491  46 
val generic_theory: (generic_theory > generic_theory) > transition > transition 
7612  47 
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

48 
val theory: (theory > theory) > transition > transition 
20985  49 
val begin_local_theory: bool > (theory > local_theory) > transition > transition 
21007  50 
val end_local_theory: transition > transition 
47069  51 
val open_target: (generic_theory > local_theory) > transition > transition 
52 
val close_target: transition > transition 

59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59923
diff
changeset

53 
val local_theory': (bool * Position.T) option > (xstring * Position.T) option > 
59923
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59472
diff
changeset

54 
(bool > local_theory > local_theory) > transition > transition 
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59923
diff
changeset

55 
val local_theory: (bool * Position.T) option > (xstring * Position.T) option > 
59923
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59472
diff
changeset

56 
(local_theory > local_theory) > transition > transition 
45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset

57 
val present_local_theory: (xstring * Position.T) option > (state > unit) > 
24453  58 
transition > transition 
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59923
diff
changeset

59 
val local_theory_to_proof': (bool * Position.T) option > (xstring * Position.T) option > 
45488
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset

60 
(bool > local_theory > Proof.state) > transition > transition 
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59923
diff
changeset

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

62 
(local_theory > Proof.state) > transition > transition 
17363  63 
val theory_to_proof: (theory > Proof.state) > transition > transition 
21007  64 
val end_proof: (bool > Proof.state > Proof.context) > transition > transition 
58798
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58795
diff
changeset

65 
val forget_proof: bool > transition > transition 
49863
b5fb6e7f8d81
more informative errors for 'proof' and 'apply' steps;
wenzelm
parents:
49062
diff
changeset

66 
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

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

68 
val proofs: (Proof.state > Proof.state Seq.result Seq.seq) > transition > transition 
21177  69 
val proof: (Proof.state > Proof.state) > transition > transition 
33390  70 
val actual_proof: (Proof_Node.T > Proof_Node.T) > transition > transition 
60693
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

71 
val skip_proof: (unit > unit) > transition > transition 
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

72 
val skip_proof_open: transition > transition 
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

73 
val skip_proof_close: transition > transition 
52536  74 
val exec_id: Document_ID.exec > transition > transition 
28425  75 
val setmp_thread_position: transition > ('a > 'b) > 'a > 'b 
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset

76 
val add_hook: (transition > state > state > unit) > unit 
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

77 
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

78 
val put_timing: Time.time option > transition > transition 
59055
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
59032
diff
changeset

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

81 
val command_exception: bool > transition > state > state 
56937  82 
val reset_theory: state > state option 
83 
val reset_proof: state > state option 

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

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

85 
val join_results: result > (transition * state) list 
58923  86 
val element_result: Keyword.keywords > transition Thy_Syntax.element > state > result * state 
5828  87 
end; 
88 

6965  89 
structure Toplevel: TOPLEVEL = 
5828  90 
struct 
91 

92 
(** toplevel state **) 

93 

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

94 
exception UNDEF = Runtime.UNDEF; 
19063  95 

96 

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

97 
(* datatype node *) 
21294  98 

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

100 
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

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

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

105 
(*proof depth, resulting theory, original theory*) 
5828  106 

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

107 
val theory_node = fn Theory (gthy, _) => SOME gthy  _ => NONE; 
18589  108 
val proof_node = fn Proof (prf, _) => SOME prf  _ => NONE; 
51555  109 
val skipped_proof_node = fn Skipped_Proof _ => true  _ => false; 
18589  110 

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

111 
fun cases_node f _ (Theory (gthy, _)) = f gthy 
33390  112 
 cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf) 
51555  113 
 cases_node f _ (Skipped_Proof (_, (gthy, _))) = f gthy; 
19063  114 

29066  115 
val context_node = cases_node Context.proof_of Proof.context_of; 
116 

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

117 

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

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

119 

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

120 
datatype state = State of node option * node option; (*current, previous*) 
5828  121 

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

122 
val toplevel = State (NONE, NONE); 
5828  123 

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

124 
fun is_toplevel (State (NONE, _)) = true 
7732  125 
 is_toplevel _ = false; 
126 

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

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

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

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

52565  132 
fun str_of_state (State (NONE, SOME (Theory (Context.Theory thy, _)))) = 
133 
"at top level, result theory " ^ quote (Context.theory_name thy) 

134 
 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

135 
 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

136 
 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

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

139 

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

140 

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

141 
(* current node *) 
5828  142 

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

143 
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

144 
 node_of (State (SOME node, _)) = node; 
5828  145 

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

51555  148 
fun is_skipped_proof state = not (is_toplevel state) andalso skipped_proof_node (node_of state); 
18589  149 

19063  150 
fun node_case f g state = cases_node f g (node_of state); 
5828  151 

30398  152 
fun presentation_context_of state = 
153 
(case try node_of state of 

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

155 
 SOME node => context_node node 

156 
 NONE => raise UNDEF); 

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

157 

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

159 
 previous_context_of (State (_, SOME prev)) = SOME (context_node prev); 
30801  160 

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

163 
val theory_of = node_case Context.theory_of Proof.theory_of; 
60094  164 
val proof_of = node_case (fn _ => error "No proof state") I; 
17208  165 

18589  166 
fun proof_position_of state = 
167 
(case node_of state of 

33390  168 
Proof (prf, _) => Proof_Node.position prf 
60094  169 
 _ => ~1); 
6664  170 

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

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

174 

5828  175 

16815  176 
(* print state *) 
177 

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

179 
(case try node_of state of 
21506  180 
NONE => [] 
56893  181 
 SOME node => 
182 
let 

183 
val gthy = 

184 
(case node of 

185 
Theory (gthy, _) => gthy 

186 
 Proof (_, (_, gthy)) => gthy 

187 
 Skipped_Proof (_, (gthy, _)) => gthy); 

188 
val lthy = Context.cases (Named_Target.theory_init) I gthy; 

189 
in Local_Theory.pretty lthy end); 

16815  190 

56887
1ca814da47ae
clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;
wenzelm
parents:
56867
diff
changeset

191 
fun pretty_state state = 
23701  192 
(case try node_of state of 
193 
NONE => [] 

56887
1ca814da47ae
clarified print_state, which goes back to TTY loop before Proof General, and before separate print_context;
wenzelm
parents:
56867
diff
changeset

194 
 SOME (Theory _) => [] 
60403  195 
 SOME (Proof (prf, _)) => Proof.pretty_state (Proof_Node.current prf) 
56867  196 
 SOME (Skipped_Proof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]); 
197 

61208  198 
val string_of_state = pretty_state #> Pretty.chunks #> Pretty.string_of; 
16815  199 

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

62663  202 
val _ = PolyML.addPrettyPrinter (fn _ => fn _ => Pretty.to_polyml o pretty_abstract); 
203 

16815  204 

15668  205 

5828  206 
(** toplevel transitions **) 
207 

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

208 
(* node transactions  maintaining stable checkpoints *) 
7022  209 

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

210 
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

211 

6689  212 
local 
213 

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

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

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

216 

6689  217 
in 
218 

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

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

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

221 
val cont_node = reset_presentation node; 
56265
785569927666
discontinued Toplevel.debug in favour of system option "exception_trace";
wenzelm
parents:
56147
diff
changeset

222 
val context = cases_node I (Context.Proof o Proof.context_of) cont_node; 
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

223 
fun state_error e nd = (State (SOME nd, SOME node), e); 
6689  224 

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

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

226 
cont_node 
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56265
diff
changeset

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

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

229 
handle exn => state_error (SOME exn) cont_node; 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

230 
in 
52696
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52565
diff
changeset

231 
(case err of 
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52565
diff
changeset

232 
NONE => tap g result 
38466f4f3483
immutable theory values with full stamp record of every update (increase of stamp size for HOL: 20000 > 100000, JinjaThreads: 65000 > 300000)  minimal measurable impact on inference kernel performance;
wenzelm
parents:
52565
diff
changeset

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

234 
end; 
6689  235 

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

236 
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

237 
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

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

239 
 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

240 
#> (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

241 

6689  242 
end; 
243 

244 

245 
(* primitive transitions *) 

246 

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

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

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

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

251 
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

252 

6689  253 
local 
5828  254 

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

255 
fun apply_tr _ (Init f) (State (NONE, _)) = 
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56265
diff
changeset

256 
State (SOME (Theory (Context.Theory (Runtime.controlled_execution NONE 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

257 
 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

258 
exit_transaction state 
32792  259 
 apply_tr int (Keep f) state = 
56303
4cc3f4db3447
clarified Isabelle/ML bootstrap, such that Execution does not require ML_Compiler;
wenzelm
parents:
56265
diff
changeset

260 
Runtime.controlled_execution (try generic_theory_of state) (fn x => tap (f int) x) state 
32792  261 
 apply_tr int (Transaction (f, g)) (State (SOME state, _)) = 
262 
apply_transaction (fn x => f int x) g state 

263 
 apply_tr _ _ _ = raise UNDEF; 

5828  264 

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

267 
apply_union int trs state 

268 
handle Runtime.UNDEF => apply_tr int tr state 

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

6689  270 
 exn as FAILURE _ => raise exn 
271 
 exn => raise FAILURE (state, exn); 

272 

273 
in 

274 

32792  275 
fun apply_trans int trs state = (apply_union int trs state, NONE) 
15531  276 
handle FAILURE (alt_state, exn) => (alt_state, SOME exn)  exn => (state, SOME exn); 
6689  277 

278 
end; 

5828  279 

280 

281 
(* datatype transition *) 

282 

283 
datatype transition = Transition of 

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

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

285 
pos: Position.T, (*source position*) 
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

286 
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

287 
trans: trans list}; (*primitive transitions (union)*) 
5828  288 

58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

289 
fun make_transition (name, pos, timing, trans) = 
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

290 
Transition {name = name, pos = pos, timing = timing, trans = trans}; 
5828  291 

58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

292 
fun map_transition f (Transition {name, pos, timing, trans}) = 
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

293 
make_transition (f (name, pos, timing, trans)); 
5828  294 

58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

295 
val empty = make_transition ("", Position.none, NONE, []); 
5828  296 

297 

298 
(* diagnostics *) 

299 

27427  300 
fun name_of (Transition {name, ...}) = name; 
28105  301 
fun pos_of (Transition {pos, ...}) = pos; 
5828  302 

60076  303 
fun command_msg msg tr = 
304 
msg ^ "command " ^ quote (Markup.markup Markup.keyword1 (name_of tr)) ^ 

305 
Position.here (pos_of tr); 

5828  306 

60076  307 
fun at_command tr = command_msg "At " tr; 
308 
fun type_error tr = command_msg "Bad context for " tr; 

5828  309 

310 

311 
(* modify transitions *) 

312 

58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

313 
fun name name = map_transition (fn (_, pos, timing, trans) => 
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

314 
(name, pos, timing, trans)); 
9010  315 

58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

316 
fun position pos = map_transition (fn (name, _, timing, trans) => 
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

317 
(name, pos, timing, trans)); 
14923  318 

58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

319 
fun add_trans tr = map_transition (fn (name, pos, timing, trans) => 
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

320 
(name, pos, timing, tr :: trans)); 
16607  321 

58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

322 
val reset_trans = map_transition (fn (name, pos, timing, _) => 
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

323 
(name, pos, timing, [])); 
5828  324 

325 

21007  326 
(* basic transitions *) 
5828  327 

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

328 
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

329 

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

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

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

332 

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

333 
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

334 

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

337 

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

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

339 
fun transaction f = present_transaction f (K ()); 
5828  340 

7612  341 
fun keep f = add_trans (Keep (fn _ => f)); 
5828  342 

60190
906de96ba68a
allow diagnostic proof commands with skip_proofs;
wenzelm
parents:
60189
diff
changeset

343 
fun keep_proof f = 
906de96ba68a
allow diagnostic proof commands with skip_proofs;
wenzelm
parents:
60189
diff
changeset

344 
keep (fn st => 
906de96ba68a
allow diagnostic proof commands with skip_proofs;
wenzelm
parents:
60189
diff
changeset

345 
if is_proof st then f st 
906de96ba68a
allow diagnostic proof commands with skip_proofs;
wenzelm
parents:
60189
diff
changeset

346 
else if is_skipped_proof st then () 
906de96ba68a
allow diagnostic proof commands with skip_proofs;
wenzelm
parents:
60189
diff
changeset

347 
else warning "No proof state"); 
906de96ba68a
allow diagnostic proof commands with skip_proofs;
wenzelm
parents:
60189
diff
changeset

348 

60189  349 
fun ignored pos = empty > name "<ignored>" > position pos > keep (fn _ => ()); 
51268
fcc4b89a600d
simplified Outer_Syntax.read_span: internalized Toplevel.is_ignored;
wenzelm
parents:
51241
diff
changeset

350 
fun is_ignored tr = name_of tr = "<ignored>"; 
48772  351 

27840  352 
fun malformed pos msg = 
60189  353 
empty > name "<malformed>" > position pos > keep (fn _ => error msg); 
27840  354 

21007  355 

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

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

357 

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

358 
fun generic_theory f = transaction (fn _ => 
26491  359 
(fn Theory (gthy, _) => Theory (f gthy, NONE) 
360 
 _ => raise UNDEF)); 

361 

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

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

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

364 
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

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

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

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

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

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

370 

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

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

372 

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

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

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

375 
let 
20985  376 
val lthy = f thy; 
57483
950dc7446454
centralized (adhoc) switching of targets in named_target.ML
haftmann
parents:
57184
diff
changeset

377 
val gthy = if begin then Context.Proof lthy else Context.Theory (Named_Target.exit lthy); 
56897
c668735fb8b5
print results as "state", to avoid intrusion into the source text;
wenzelm
parents:
56895
diff
changeset

378 
val _ = 
60245  379 
(case Local_Theory.pretty lthy of 
380 
[] => () 

381 
 prts => Output.state (Pretty.string_of (Pretty.chunks prts))); 

21294  382 
in Theory (gthy, SOME lthy) end 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

383 
 _ => raise UNDEF)); 
17076  384 

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

385 
val end_local_theory = transaction (fn _ => 
57483
950dc7446454
centralized (adhoc) switching of targets in named_target.ML
haftmann
parents:
57184
diff
changeset

386 
(fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (Named_Target.exit lthy), SOME lthy) 
21007  387 
 _ => raise UNDEF)); 
388 

47069  389 
fun open_target f = transaction (fn _ => 
390 
(fn Theory (gthy, _) => 

391 
let val lthy = f gthy 

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

393 
 _ => raise UNDEF)); 

394 

395 
val close_target = transaction (fn _ => 

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

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

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

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

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

401 
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

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

403 
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

404 
in Theory (gthy', SOME lthy) end 
47069  405 
 NONE => raise UNDEF) 
406 
 _ => raise UNDEF)); 

407 

59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59939
diff
changeset

408 
fun restricted_context (SOME (strict, scope)) = 
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59939
diff
changeset

409 
Proof_Context.map_naming (Name_Space.restricted strict scope) 
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59939
diff
changeset

410 
 restricted_context NONE = I; 
59939
7d46aa03696e
support for 'restricted' modifier: only qualified accesses outside the local scope;
wenzelm
parents:
59923
diff
changeset

411 

59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59939
diff
changeset

412 
fun local_theory' restricted target f = present_transaction (fn int => 
21294  413 
(fn Theory (gthy, _) => 
414 
let 

59923
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59472
diff
changeset

415 
val (finish, lthy) = Named_Target.switch target gthy; 
47274  416 
val lthy' = lthy 
59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59939
diff
changeset

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

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

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

420 
> Local_Theory.reset_group; 
21294  421 
in Theory (finish lthy', SOME lthy') end 
59032  422 
 _ => raise UNDEF)) 
423 
(K ()); 

15668  424 

59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59939
diff
changeset

425 
fun local_theory restricted target f = local_theory' restricted target (K f); 
21007  426 

59923
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59472
diff
changeset

427 
fun present_local_theory target = present_transaction (fn int => 
59032  428 
(fn Theory (gthy, _) => 
59923
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59472
diff
changeset

429 
let val (finish, lthy) = Named_Target.switch target gthy; 
59032  430 
in Theory (finish lthy, SOME lthy) end 
431 
 _ => raise UNDEF)); 

21007  432 

433 

434 
(* proof transitions *) 

435 

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

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

437 
(fn Proof (prf, (finish, _)) => 
33390  438 
let val state = Proof_Node.current prf in 
21007  439 
if can (Proof.assert_bottom true) state then 
440 
let 

441 
val ctxt' = f int state; 

442 
val gthy' = finish ctxt'; 

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

444 
else raise UNDEF 

445 
end 

51555  446 
 Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE) 
21007  447 
 _ => raise UNDEF)); 
448 

21294  449 
local 
450 

47274  451 
fun begin_proof init = transaction (fn int => 
21294  452 
(fn Theory (gthy, _) => 
453 
let 

47274  454 
val (finish, prf) = init int gthy; 
52499  455 
val skip = Goal.skip_proofs_enabled (); 
58795  456 
val schematic_goal = try Proof.schematic_goal prf; 
47274  457 
val _ = 
58795  458 
if skip andalso schematic_goal = SOME true then 
47274  459 
warning "Cannot skip proof of schematic goal statement" 
460 
else (); 

21294  461 
in 
58795  462 
if skip andalso schematic_goal = SOME false then 
51555  463 
Skipped_Proof (0, (finish (Proof.global_skip_proof true prf), gthy)) 
47274  464 
else Proof (Proof_Node.init prf, (finish, gthy)) 
21294  465 
end 
466 
 _ => raise UNDEF)); 

467 

468 
in 

469 

59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59939
diff
changeset

470 
fun local_theory_to_proof' restricted target f = begin_proof 
47274  471 
(fn int => fn gthy => 
59923
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59472
diff
changeset

472 
let 
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59472
diff
changeset

473 
val (finish, lthy) = Named_Target.switch target gthy; 
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59472
diff
changeset

474 
val prf = lthy 
59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59939
diff
changeset

475 
> restricted_context restricted 
59923
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59472
diff
changeset

476 
> Local_Theory.new_group 
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59472
diff
changeset

477 
> f int; 
b21c82422d65
support private scope for individual local theory commands;
wenzelm
parents:
59472
diff
changeset

478 
in (finish o Local_Theory.reset_group, prf) end); 
24780
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset

479 

59990
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59939
diff
changeset

480 
fun local_theory_to_proof restricted target f = 
a81dc82ecba3
clarified keyword 'qualified' in accordance to a similar keyword from Haskell (despite unrelated Binding.qualified in Isabelle/ML);
wenzelm
parents:
59939
diff
changeset

481 
local_theory_to_proof' restricted target (K f); 
21294  482 

483 
fun theory_to_proof f = begin_proof 

47274  484 
(fn _ => fn gthy => 
56057
ad6bd8030d88
more explicit Sign.change_check  detect structural mistakes where they emerge, not at later theory merges;
wenzelm
parents:
56055
diff
changeset

485 
(Context.Theory o Sign.reset_group o Sign.change_check o Proof_Context.theory_of, 
49062
7e31dfd99ce7
discontinued complicated/unreliable notion of recent proofs within context;
wenzelm
parents:
49042
diff
changeset

486 
(case gthy of 
52788  487 
Context.Theory thy => f (Sign.new_group thy) 
49012
8686c36fa27d
refined treatment of forked proofs at transaction boundaries, including proof commands (see also 7ee000ce5390);
wenzelm
parents:
49011
diff
changeset

488 
 _ => raise UNDEF))); 
21294  489 

490 
end; 

491 

58798
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58795
diff
changeset

492 
fun forget_proof strict = transaction (fn _ => 
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58795
diff
changeset

493 
(fn Proof (prf, (_, orig_gthy)) => 
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58795
diff
changeset

494 
if strict andalso not (Proof.has_bottom_goal (Proof_Node.current prf)) 
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58795
diff
changeset

495 
then raise UNDEF else Theory (orig_gthy, NONE) 
51555  496 
 Skipped_Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 
21007  497 
 _ => raise UNDEF)); 
498 

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

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

500 
(fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) 
51555  501 
 skip as Skipped_Proof _ => skip 
16815  502 
 _ => raise UNDEF)); 
15668  503 

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

504 
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

505 
val proofs = proofs' o K; 
6689  506 
val proof = proof' o K; 
16815  507 

60693
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

508 

044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

509 
(* skipped proofs *) 
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

510 

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

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

513 
 _ => raise UNDEF)); 
16815  514 

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

515 
fun skip_proof f = transaction (fn _ => 
60693
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

516 
(fn skip as Skipped_Proof _ => (f (); skip) 
18563  517 
 _ => raise UNDEF)); 
518 

60693
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

519 
val skip_proof_open = transaction (fn _ => 
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

520 
(fn Skipped_Proof (d, x) => Skipped_Proof (d + 1, x) 
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

521 
 _ => raise UNDEF)); 
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

522 

044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

523 
val skip_proof_close = transaction (fn _ => 
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

524 
(fn Skipped_Proof (0, (gthy, _)) => Theory (gthy, NONE) 
044f8bb3dd30
more accurate skip_proofs nesting, e.g. relevant for 'subgoal' command;
wenzelm
parents:
60403
diff
changeset

525 
 Skipped_Proof (d, x) => Skipped_Proof (d  1, x) 
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

526 
 _ => raise UNDEF)); 
5828  527 

528 

529 

530 
(** toplevel transactions **) 

531 

52527
dbac84eab3bc
separate exec_id assignment for Command.print states, without affecting result of eval;
wenzelm
parents:
52499
diff
changeset

532 
(* runtime position *) 
27427  533 

52536  534 
fun exec_id id (tr as Transition {pos, ...}) = 
535 
position (Position.put_id (Document_ID.print id) pos) tr; 

25799  536 

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

538 
Position.setmp_thread_data pos f x; 
25799  539 

540 

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

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

542 

37905  543 
local 
56147  544 
val hooks = 
545 
Synchronized.var "Toplevel.hooks" ([]: (transition > state > state > unit) list); 

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

547 

56147  548 
fun add_hook hook = Synchronized.change hooks (cons hook); 
549 
fun get_hooks () = Synchronized.value hooks; 

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

550 

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

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

552 

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

553 

5828  554 
(* apply transitions *) 
555 

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

556 
fun get_timing (Transition {timing, ...}) = timing; 
58893
9e0ecb66d6a7
eliminated unused int_only flag (see also c12484a27367);
wenzelm
parents:
58849
diff
changeset

557 
fun put_timing timing = map_transition (fn (name, pos, _, trans) => (name, pos, timing, trans)); 
51217
65ab2c4f4c32
support for prescient timing information within command transactions;
wenzelm
parents:
51216
diff
changeset

558 

6664  559 
local 
560 

56895
f058120aaad4
discontinued Toplevel.print flag  print uniformly according to Keyword.is_printed;
wenzelm
parents:
56893
diff
changeset

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

562 
setmp_thread_position tr (fn state => 
25799  563 
let 
51595  564 
val timing_start = Timing.start (); 
61884
d4c89ea5e6dc
discontinued builtin profiling: avoid danger of conflicting invocations (multithreading etc.);
wenzelm
parents:
61208
diff
changeset

565 
val (result, opt_err) = apply_trans int trans state; 
51595  566 
val timing_result = Timing.result timing_start; 
51662
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset

567 
val timing_props = 
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset

568 
Markup.command_timing :: (Markup.nameN, name_of tr) :: Position.properties_of (pos_of tr); 
3391a493f39a
just one timing protocol function, with 3 implementations: TTY/PG, PIDE/document, build;
wenzelm
parents:
51661
diff
changeset

569 
val _ = Timing.protocol_message timing_props timing_result; 
60076  570 
in (result, Option.map (fn UNDEF => ERROR (type_error tr)  exn => exn) opt_err) end); 
6664  571 

572 
in 

5828  573 

26602
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

574 
fun transition int tr st = 
28095
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

575 
let 
60895
501be4aa75b4
default ML context for all command transactions, e.g. relevant for debugging and toplevel prettyprinting;
wenzelm
parents:
60693
diff
changeset

576 
val (st', opt_err) = 
501be4aa75b4
default ML context for all command transactions, e.g. relevant for debugging and toplevel prettyprinting;
wenzelm
parents:
60693
diff
changeset

577 
Context.setmp_thread_data (try (Context.Proof o presentation_context_of) st) 
501be4aa75b4
default ML context for all command transactions, e.g. relevant for debugging and toplevel prettyprinting;
wenzelm
parents:
60693
diff
changeset

578 
(fn () => app int tr st) (); 
59055
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
59032
diff
changeset

579 
val opt_err' = opt_err > Option.map 
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
59032
diff
changeset

580 
(fn Runtime.EXCURSION_FAIL exn_info => exn_info 
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
59032
diff
changeset

581 
 exn => (Runtime.exn_context (try context_of st) exn, at_command tr)); 
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
59032
diff
changeset

582 
val _ = get_hooks () > List.app (fn f => (try (fn () => f tr st st') (); ())); 
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
59032
diff
changeset

583 
in (st', opt_err') end; 
6664  584 

585 
end; 

5828  586 

587 

51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51282
diff
changeset

588 
(* managed commands *) 
5828  589 

51323  590 
fun command_errors int tr st = 
591 
(case transition int tr st of 

59055
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
59032
diff
changeset

592 
(st', NONE) => ([], SOME st') 
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
59032
diff
changeset

593 
 (_, SOME (exn, _)) => (Runtime.exn_messages_ids exn, NONE)); 
51323  594 

51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51282
diff
changeset

595 
fun command_exception int tr st = 
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51282
diff
changeset

596 
(case transition int tr st of 
59055
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
59032
diff
changeset

597 
(st', NONE) => st' 
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
59032
diff
changeset

598 
 (_, SOME (exn, info)) => 
62505  599 
if Exn.is_interrupt exn then Exn.reraise exn 
59055
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
59032
diff
changeset

600 
else raise Runtime.EXCURSION_FAIL (exn, info)); 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

601 

58848  602 
val command = command_exception false; 
51284
59a03019f3bf
fork diagnostic commands (theory loader and PIDE interaction);
wenzelm
parents:
51282
diff
changeset

603 

28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

604 

56937  605 
(* reset state *) 
606 

607 
local 

608 

609 
fun reset_state check trans st = 

610 
if check st then NONE 

611 
else #2 (command_errors false (trans empty) st); 

612 

613 
in 

614 

58798
49ed5eea15d4
'oops' requires proper goal statement  exclude 'notepad' to avoid disrupting begin/end structure;
wenzelm
parents:
58795
diff
changeset

615 
val reset_theory = reset_state is_theory (forget_proof false); 
56937  616 

617 
val reset_proof = 

618 
reset_state is_proof 

619 
(transaction (fn _ => 

620 
(fn Theory (gthy, _) => Skipped_Proof (0, (gthy, gthy)) 

621 
 _ => raise UNDEF))); 

622 

623 
end; 

624 

625 

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

626 
(* scheduled proof result *) 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

627 

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

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

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

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

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

632 

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

633 
fun join_results (Result x) = [x] 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

634 
 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

635 
 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

636 

51323  637 
local 
638 

47417  639 
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

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

641 
type T = result; 
59150  642 
fun init _ = Result_List []; 
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

643 
); 
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

644 

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

645 
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

646 
val put_result = Proof.map_context o Result.put; 
51324  647 

51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

648 
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

649 
let 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

650 
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

651 
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

652 
in 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

653 
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

654 
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

655 
else NONE 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

656 
end; 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

657 

e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

658 
fun priority NONE = ~1 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

659 
 priority (SOME estimate) = 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

660 
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

661 

e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

662 
fun proof_future_enabled estimate st = 
51324  663 
(case try proof_of st of 
664 
NONE => false 

665 
 SOME state => 

666 
not (Proof.is_relevant state) andalso 

667 
(if can (Proof.assert_bottom true) state 

53189
ee8b8dafef0e
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
wenzelm
parents:
52788
diff
changeset

668 
then Goal.future_enabled 1 
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

669 
else 
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

670 
(case estimate of 
53189
ee8b8dafef0e
discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
wenzelm
parents:
52788
diff
changeset

671 
NONE => Goal.future_enabled 2 
51423
e5f9a6d9ca82
clarified parallel_subproofs_saturation (blind guess) vs. parallel_subproofs_threshold (precient timing estimate);
wenzelm
parents:
51332
diff
changeset

672 
 SOME t => Goal.future_enabled_timing t))); 
51278  673 

58923  674 
fun atom_result keywords tr st = 
51323  675 
let 
676 
val st' = 

58923  677 
if Goal.future_enabled 1 andalso Keyword.is_diag keywords (name_of tr) then 
53192  678 
(Execution.fork 
51605
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

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

680 
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

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

683 
in (Result (tr, st'), st') end; 
51323  684 

685 
in 

686 

58923  687 
fun element_result keywords (Thy_Syntax.Element (tr, NONE)) st = atom_result keywords tr st 
688 
 element_result keywords (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

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

691 
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

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

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

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

697 
val proof_trs = maps Thy_Syntax.flat_element body_elems @ [end_tr]; 
58923  698 
val (proof_results, st'') = fold_map (atom_result keywords) proof_trs st'; 
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

699 
in (Result_List (head_result :: proof_results), st'') end 
51324  700 
else 
701 
let 

702 
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

703 

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

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

705 
Proof.future_proof (fn state => 
53192  706 
Execution.fork 
51605
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

707 
{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

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

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

710 
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

711 
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

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

713 
State (SOME (Proof (prf', (finish, orig_gthy))), prev) 
58923  714 
> fold_map (element_result keywords) body_elems > command end_tr; 
51605
eca8acb42e4a
more explicit Goal.fork_params  avoid implicit arguments via thread data;
wenzelm
parents:
51595
diff
changeset

715 
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

716 
#> (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

717 

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

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

719 
proof (future_proof #> 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

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

721 
end_proof (fn _ => future_proof #> 
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

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

723 

51324  724 
val st'' = st' 
56895
f058120aaad4
discontinued Toplevel.print flag  print uniformly according to Keyword.is_printed;
wenzelm
parents:
56893
diff
changeset

725 
> command (head_tr > reset_trans > forked_proof); 
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

726 
val end_result = Result (end_tr, st''); 
51324  727 
val result = 
51332
8707df0b0255
refined parallel_proofs = 2: fork whole Isar subproofs, not just terminal ones;
wenzelm
parents:
51324
diff
changeset

728 
Result_List [head_result, Result.get (presentation_context_of st''), end_result]; 
51324  729 
in (result, st'') end 
730 
end; 

28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

731 

6664  732 
end; 
51323  733 

734 
end; 