author  wenzelm 
Wed, 29 Aug 2012 11:48:45 +0200  
changeset 48992  0518bf89c777 
parent 48772  e46cd0d26481 
child 48993  44428ea53dc1 
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 

17076  15 
val level: state > int 
30398  16 
val presentation_context_of: state > Proof.context 
30801  17 
val previous_context_of: state > Proof.context option 
21506  18 
val context_of: state > Proof.context 
22089  19 
val generic_theory_of: state > generic_theory 
5828  20 
val theory_of: state > theory 
21 
val proof_of: state > Proof.state 

18589  22 
val proof_position_of: state > int 
37953
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

23 
val end_theory: Position.T > state > theory 
16815  24 
val print_state_context: state > unit 
25 
val print_state: bool > state > unit 

37858  26 
val pretty_abstract: state > Pretty.T 
32738  27 
val quiet: bool Unsynchronized.ref 
28 
val debug: bool Unsynchronized.ref 

29 
val interact: bool Unsynchronized.ref 

30 
val timing: bool Unsynchronized.ref 

31 
val profiling: int Unsynchronized.ref 

32 
val skip_proofs: bool Unsynchronized.ref 

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

33 
val program: (unit > 'a) > 'a 
33604
d4220df6fde2
Toplevel.thread provides 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 
27500  40 
val str_of: transition > string 
5828  41 
val name: string > transition > transition 
42 
val position: Position.T > transition > transition 

43 
val interactive: bool > transition > transition 

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

44 
val set_print: bool > transition > transition 
5828  45 
val print: transition > transition 
9010  46 
val no_timing: transition > transition 
44187
88d770052bac
simplified Toplevel.init_theory: discontinued special name argument;
wenzelm
parents:
44186
diff
changeset

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

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

49 
val modify_init: (unit > theory) > transition > transition 
6689  50 
val exit: transition > transition 
5828  51 
val keep: (state > unit) > transition > transition 
7612  52 
val keep': (bool > state > unit) > transition > transition 
5828  53 
val imperative: (unit > unit) > transition > transition 
27840  54 
val ignored: Position.T > transition 
55 
val malformed: Position.T > string > transition 

48772  56 
val is_malformed: transition > bool 
5828  57 
val theory: (theory > theory) > transition > transition 
26491  58 
val generic_theory: (generic_theory > generic_theory) > transition > transition 
7612  59 
val theory': (bool > theory > theory) > transition > transition 
20985  60 
val begin_local_theory: bool > (theory > local_theory) > transition > transition 
21007  61 
val end_local_theory: transition > transition 
47069  62 
val open_target: (generic_theory > local_theory) > transition > transition 
63 
val close_target: transition > transition 

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

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

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

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

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

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

71 
(bool > local_theory > Proof.state) > transition > transition 
6d71d9e52369
pass positions for named targets, for formal links in the document model;
wenzelm
parents:
44304
diff
changeset

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

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

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

77 
val present_proof: (state > unit) > transition > transition 
21177  78 
val proofs': (bool > Proof.state > Proof.state Seq.seq) > transition > transition 
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

79 
val proof': (bool > Proof.state > Proof.state) > transition > transition 
21177  80 
val proofs: (Proof.state > Proof.state Seq.seq) > transition > transition 
81 
val proof: (Proof.state > Proof.state) > transition > transition 

33390  82 
val actual_proof: (Proof_Node.T > Proof_Node.T) > transition > transition 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

83 
val skip_proof: (int > int) > transition > transition 
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

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

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

89 
val unknown_context: transition > transition 

28425  90 
val setmp_thread_position: transition > ('a > 'b) > 'a > 'b 
27606  91 
val status: transition > Markup.T > unit 
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44200
diff
changeset

92 
val error_msg: transition > serial * string > unit 
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset

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

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

96 
val proof_result: bool > transition * transition list > state > 
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

97 
(transition * state) list future * state 
5828  98 
end; 
99 

6965  100 
structure Toplevel: TOPLEVEL = 
5828  101 
struct 
102 

103 
(** toplevel state **) 

104 

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

105 
exception UNDEF = Runtime.UNDEF; 
19063  106 

107 

21294  108 
(* local theory wrappers *) 
5828  109 

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

110 
val loc_init = Named_Target.context_cmd; 
47069  111 
val loc_exit = Local_Theory.assert_bottom true #> Local_Theory.exit_global; 
21294  112 

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

115 
 loc_begin NONE (Context.Proof lthy) = 

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

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

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

21294  119 

120 

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

121 
(* datatype node *) 
21294  122 

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

124 
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

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

127 
(*proof node, finish, original theory*)  
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

128 
SkipProof of int * (generic_theory * generic_theory); 
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

129 
(*proof depth, resulting theory, original theory*) 
5828  130 

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

131 
val theory_node = fn Theory (gthy, _) => SOME gthy  _ => NONE; 
18589  132 
val proof_node = fn Proof (prf, _) => SOME prf  _ => NONE; 
133 

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

134 
fun cases_node f _ (Theory (gthy, _)) = f gthy 
33390  135 
 cases_node _ g (Proof (prf, _)) = g (Proof_Node.current prf) 
21007  136 
 cases_node f _ (SkipProof (_, (gthy, _))) = f gthy; 
19063  137 

29066  138 
val context_node = cases_node Context.proof_of Proof.context_of; 
139 

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

140 

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

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

142 

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

143 
datatype state = State of node option * node option; (*current, previous*) 
5828  144 

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

145 
val toplevel = State (NONE, NONE); 
5828  146 

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

147 
fun is_toplevel (State (NONE, _)) = true 
7732  148 
 is_toplevel _ = false; 
149 

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

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

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

152 
 level (State (SOME (Proof (prf, _)), _)) = Proof.level (Proof_Node.current prf) 
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

153 
 level (State (SOME (SkipProof (d, _)), _)) = d + 1; (*different notion of proof depth!*) 
17076  154 

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

155 
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

156 
 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

157 
 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

158 
 str_of_state (State (SOME (Proof _), _)) = "in proof mode" 
ddc3b72f9a42
simplified handling of theory begin/end wrt. toplevel and theory loader;
wenzelm
parents:
37951
diff
changeset

159 
 str_of_state (State (SOME (SkipProof _), _)) = "in skipped proof mode"; 
5946
a4600d21b59b
print_state hook, obeys Goals.current_goals_markers by default;
wenzelm
parents:
5939
diff
changeset

160 

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

161 

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

162 
(* current node *) 
5828  163 

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

164 
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

165 
 node_of (State (SOME node, _)) = node; 
5828  166 

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

169 

19063  170 
fun node_case f g state = cases_node f g (node_of state); 
5828  171 

30398  172 
fun presentation_context_of state = 
173 
(case try node_of state of 

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

175 
 SOME node => context_node node 

176 
 NONE => raise UNDEF); 

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

177 

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

179 
 previous_context_of (State (_, SOME prev)) = SOME (context_node prev); 
30801  180 

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

183 
val theory_of = node_case Context.theory_of Proof.theory_of; 
18589  184 
val proof_of = node_case (fn _ => raise UNDEF) I; 
17208  185 

18589  186 
fun proof_position_of state = 
187 
(case node_of state of 

33390  188 
Proof (prf, _) => Proof_Node.position prf 
18589  189 
 _ => raise UNDEF); 
6664  190 

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

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

194 

5828  195 

16815  196 
(* print state *) 
197 

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

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

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

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

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

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

205 
 SOME (SkipProof (_, (gthy, _))) => pretty_context gthy) 
23640
baec2e674461
toplevel prompt/print_state: proper markup, removed hooks;
wenzelm
parents:
23619
diff
changeset

206 
> Pretty.chunks > Pretty.writeln; 
16815  207 

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

208 
fun print_state prf_only state = 
23701  209 
(case try node_of state of 
210 
NONE => [] 

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

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

33390  213 
Proof.pretty_state (Proof_Node.position prf) (Proof_Node.current prf) 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

214 
 SOME (SkipProof (d, _)) => [Pretty.str ("skipped proof: depth " ^ string_of_int d)]) 
45666  215 
> Pretty.markup_chunks Isabelle_Markup.state > Pretty.writeln; 
16815  216 

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

16815  219 

15668  220 

5828  221 
(** toplevel transitions **) 
222 

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

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

226 
val timing = Unsynchronized.ref false; 
32738  227 
val profiling = Unsynchronized.ref 0; 
228 
val skip_proofs = Unsynchronized.ref false; 

16682  229 

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

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

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

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

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

234 

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

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

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

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

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

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

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

241 
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

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

243 

5828  244 

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

245 
(* node transactions  maintaining stable checkpoints *) 
7022  246 

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

247 
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

248 

6689  249 
local 
250 

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

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

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

253 

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

254 
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

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

256 

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

257 
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

258 

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

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

260 
 stale_error some = some; 
16815  261 

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

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

264 
 map_theory _ node = node; 
6689  265 

266 
in 

267 

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

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

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

270 
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

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

272 
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

273 
fun state_error e nd = (State (SOME nd, SOME node), e); 
6689  274 

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

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

276 
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

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

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

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

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

281 

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

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

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

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

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

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

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

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

289 
end; 
6689  290 

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

291 
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

292 
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

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

294 
 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

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

296 

6689  297 
end; 
298 

299 

300 
(* primitive transitions *) 

301 

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

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

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

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

306 
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

307 

6689  308 
local 
5828  309 

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

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

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

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

313 
 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

314 
exit_transaction state 
32792  315 
 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

316 
Runtime.controlled_execution (fn x => tap (f int) x) state 
32792  317 
 apply_tr int (Transaction (f, g)) (State (SOME state, _)) = 
318 
apply_transaction (fn x => f int x) g state 

319 
 apply_tr _ _ _ = raise UNDEF; 

5828  320 

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

323 
apply_union int trs state 

324 
handle Runtime.UNDEF => apply_tr int tr state 

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

6689  326 
 exn as FAILURE _ => raise exn 
327 
 exn => raise FAILURE (state, exn); 

328 

329 
in 

330 

32792  331 
fun apply_trans int trs state = (apply_union int trs state, NONE) 
15531  332 
handle FAILURE (alt_state, exn) => (alt_state, SOME exn)  exn => (state, SOME exn); 
6689  333 

334 
end; 

5828  335 

336 

337 
(* datatype transition *) 

338 

339 
datatype transition = Transition of 

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

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

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

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

343 
print: bool, (*print result state*) 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

344 
no_timing: bool, (*suppress timing*) 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

345 
trans: trans list}; (*primitive transitions (union)*) 
5828  346 

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

347 
fun make_transition (name, pos, int_only, print, no_timing, trans) = 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

348 
Transition {name = name, pos = pos, int_only = int_only, print = print, no_timing = no_timing, 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

349 
trans = trans}; 
5828  350 

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

351 
fun map_transition f (Transition {name, pos, int_only, print, no_timing, trans}) = 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

352 
make_transition (f (name, pos, int_only, print, no_timing, trans)); 
5828  353 

27441  354 
val empty = make_transition ("", Position.none, false, false, false, []); 
5828  355 

356 

357 
(* diagnostics *) 

358 

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

359 
fun print_of (Transition {print, ...}) = print; 
27427  360 
fun name_of (Transition {name, ...}) = name; 
28105  361 
fun pos_of (Transition {pos, ...}) = pos; 
48992  362 
fun str_of tr = quote (name_of tr) ^ Position.here (pos_of tr); 
5828  363 

27427  364 
fun command_msg msg tr = msg ^ "command " ^ str_of tr; 
38875
c7a66b584147
tuned messages: discontinued spurious fullstops (messages are occasionally composed unexpectedly);
wenzelm
parents:
38721
diff
changeset

365 
fun at_command tr = command_msg "At " tr; 
5828  366 

367 
fun type_error tr state = 

18685  368 
ERROR (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); 
5828  369 

370 

371 
(* modify transitions *) 

372 

28451
0586b855c2b5
datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents:
28446
diff
changeset

373 
fun name name = map_transition (fn (_, pos, int_only, print, no_timing, trans) => 
0586b855c2b5
datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents:
28446
diff
changeset

374 
(name, pos, int_only, print, no_timing, trans)); 
9010  375 

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

376 
fun position pos = map_transition (fn (name, _, int_only, print, no_timing, trans) => 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

377 
(name, pos, int_only, print, no_timing, trans)); 
5828  378 

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

379 
fun interactive int_only = map_transition (fn (name, pos, _, print, no_timing, trans) => 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

380 
(name, pos, int_only, print, no_timing, trans)); 
14923  381 

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

382 
val no_timing = map_transition (fn (name, pos, int_only, print, _, trans) => 
78b3ad7af5d5
eliminated unused name_of, source, source_of, print', print3, three_buffersN;
wenzelm
parents:
26602
diff
changeset

383 
(name, pos, int_only, print, true, trans)); 
17363  384 

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

385 
fun add_trans tr = map_transition (fn (name, pos, int_only, print, no_timing, trans) => 
28451
0586b855c2b5
datatype transition: internal trans field is maintained in reverse order;
wenzelm
parents:
28446
diff
changeset

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

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

388 
val reset_trans = map_transition (fn (name, pos, int_only, print, no_timing, _) => 
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

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

390 

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

391 
fun set_print print = map_transition (fn (name, pos, int_only, _, no_timing, trans) => 
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

392 
(name, pos, int_only, print, no_timing, trans)); 
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

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; 
48772  416 

417 
val malformed_name = "<malformed>"; 

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

27840  421 

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

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

15668  425 

21007  426 

427 
(* theory transitions *) 

15668  428 

44304
7ee000ce5390
maintain recent future proofs at transaction boundaries;
wenzelm
parents:
44270
diff
changeset

429 
val global_theory_group = 
7ee000ce5390
maintain recent future proofs at transaction boundaries;
wenzelm
parents:
44270
diff
changeset

430 
Sign.new_group #> 
7ee000ce5390
maintain recent future proofs at transaction boundaries;
wenzelm
parents:
44270
diff
changeset

431 
Global_Theory.begin_recent_proofs #> Theory.checkpoint; 
7ee000ce5390
maintain recent future proofs at transaction boundaries;
wenzelm
parents:
44270
diff
changeset

432 

7ee000ce5390
maintain recent future proofs at transaction boundaries;
wenzelm
parents:
44270
diff
changeset

433 
val local_theory_group = 
7ee000ce5390
maintain recent future proofs at transaction boundaries;
wenzelm
parents:
44270
diff
changeset

434 
Local_Theory.new_group #> 
7ee000ce5390
maintain recent future proofs at transaction boundaries;
wenzelm
parents:
44270
diff
changeset

435 
Local_Theory.raw_theory (Global_Theory.begin_recent_proofs #> Theory.checkpoint); 
7ee000ce5390
maintain recent future proofs at transaction boundaries;
wenzelm
parents:
44270
diff
changeset

436 

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

437 
fun generic_theory f = transaction (fn _ => 
26491  438 
(fn Theory (gthy, _) => Theory (f gthy, NONE) 
439 
 _ => raise UNDEF)); 

440 

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

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

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

443 
let val thy' = thy 
44304
7ee000ce5390
maintain recent future proofs at transaction boundaries;
wenzelm
parents:
44270
diff
changeset

444 
> global_theory_group 
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

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

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

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

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

449 

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

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

451 

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

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

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

454 
let 
20985  455 
val lthy = f thy; 
21294  456 
val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy); 
457 
in Theory (gthy, SOME lthy) end 

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

458 
 _ => raise UNDEF)); 
17076  459 

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

460 
val end_local_theory = transaction (fn _ => 
21294  461 
(fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy) 
21007  462 
 _ => raise UNDEF)); 
463 

47069  464 
fun open_target f = transaction (fn _ => 
465 
(fn Theory (gthy, _) => 

466 
let val lthy = f gthy 

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

468 
 _ => raise UNDEF)); 

469 

470 
val close_target = transaction (fn _ => 

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

472 
(case try Local_Theory.close_target lthy of 

473 
SOME lthy' => Theory (Context.Proof lthy', SOME lthy) 

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 

47274  483 
val (finish, lthy) = loc_begin loc gthy; 
484 
val lthy' = lthy 

44304
7ee000ce5390
maintain recent future proofs at transaction boundaries;
wenzelm
parents:
44270
diff
changeset

485 
> local_theory_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 

27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

512 
 SkipProof (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; 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

521 
val skip = ! 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 
47274  530 
SkipProof (0, (finish (Proof.global_skip_proof int prf), gthy)) 
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 => 
539 
let val (finish, lthy) = loc_begin loc gthy 

540 
in (finish o Local_Theory.reset_group, f int (local_theory_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 => 
546 
(Context.Theory o Sign.reset_group o Proof_Context.theory_of, 

547 
(case gthy of Context.Theory thy => f (global_theory_group thy)  _ => raise UNDEF))); 

21294  548 

549 
end; 

550 

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

551 
val forget_proof = transaction (fn _ => 
21007  552 
(fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 
553 
 SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 

554 
 _ => raise UNDEF)); 

555 

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

556 
val present_proof = present_transaction (fn _ => 
33390  557 
(fn Proof (prf, x) => Proof (Proof_Node.apply I prf, x) 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

558 
 skip as SkipProof _ => skip 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

559 
 _ => raise UNDEF)); 
21177  560 

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

561 
fun proofs' f = transaction (fn int => 
33390  562 
(fn Proof (prf, x) => Proof (Proof_Node.applys (f int) prf, x) 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

563 
 skip as SkipProof _ => skip 
16815  564 
 _ => raise UNDEF)); 
15668  565 

17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

566 
fun proof' f = proofs' (Seq.single oo f); 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

567 
val proofs = proofs' o K; 
6689  568 
val proof = proof' o K; 
16815  569 

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

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

572 
 _ => raise UNDEF)); 
16815  573 

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

574 
fun skip_proof f = transaction (fn _ => 
21007  575 
(fn SkipProof (h, x) => SkipProof (f h, x) 
18563  576 
 _ => raise UNDEF)); 
577 

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

578 
fun skip_proof_to_theory pred = transaction (fn _ => 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

579 
(fn SkipProof (d, (gthy, _)) => if pred d then Theory (gthy, NONE) else raise UNDEF 
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

580 
 _ => raise UNDEF)); 
5828  581 

582 

583 

584 
(** toplevel transactions **) 

585 

27427  586 
(* identification *) 
587 

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

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

590 

591 

25960  592 
(* thread position *) 
25799  593 

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

595 
Position.setmp_thread_data pos f x; 
25799  596 

27606  597 
fun status tr m = 
43665  598 
setmp_thread_position tr (fn () => Output.status (Markup.markup_only m)) (); 
27606  599 

38876
ec7045139e70
Toplevel.run_command: more careful treatment of interrupts stemming from nested multiexceptions etc.;
wenzelm
parents:
38875
diff
changeset

600 
fun error_msg tr msg = 
44270
3eaad39e520c
more careful treatment of exception serial numbers, with propagation to message channel;
wenzelm
parents:
44200
diff
changeset

601 
setmp_thread_position tr (fn () => Output.error_msg' msg) (); 
26602
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

602 

25799  603 

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

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

605 

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

608 
in 

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

609 

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

612 

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

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

614 

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

615 

5828  616 
(* apply transitions *) 
617 

6664  618 
local 
619 

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

621 
setmp_thread_position tr (fn state => 
25799  622 
let 
623 
fun do_timing f x = (warning (command_msg "" tr); timeap f x); 

624 
fun do_profiling f x = profile (! profiling) f x; 

625 

26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

626 
val (result, status) = 
37905  627 
state > 
628 
(apply_trans int trans 

629 
> (! profiling > 0 andalso not no_timing) ? do_profiling 

630 
> (! profiling > 0 orelse ! timing andalso not no_timing) ? do_timing); 

26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

631 

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

632 
val _ = if int andalso not (! quiet) andalso print then print_state false result else (); 
26256
3e7939e978c6
added exception CONTEXT, indicating context of another exception;
wenzelm
parents:
26081
diff
changeset

633 
in (result, Option.map (fn UNDEF => type_error tr state  exn => exn) status) end); 
6664  634 

635 
in 

5828  636 

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

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

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

639 
val hooks = get_hooks (); 
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset

640 
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

641 

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

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

643 
val res = 
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

644 
(case app int tr st of 
38888
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset

645 
(_, SOME Runtime.TERMINATE) => NONE 
8248cda328de
moved Toplevel.run_command to Pure/PIDE/document.ML;
wenzelm
parents:
38876
diff
changeset

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

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

648 
 (st', NONE) => SOME (st', NONE)); 
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset

649 
val _ = (case res of SOME (st', NONE) => apply_hooks st'  _ => ()); 
28095
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

650 
in res end; 
6664  651 

652 
end; 

5828  653 

654 

28425  655 
(* nested commands *) 
5828  656 

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

658 
(case transition (! interact) tr st of 
28425  659 
SOME (st', NONE) => st' 
39285  660 
 SOME (_, SOME (exn, info)) => 
661 
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

662 
 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

663 

29483  664 
fun command_result tr st = 
665 
let val st' = command tr st 

47417  666 
in ((tr, st'), st') end; 
29483  667 

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

668 

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

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

670 

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

672 
( 
47417  673 
type T = (transition * state) list future; 
674 
val empty: T = Future.value []; 

675 
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

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

677 

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

678 
fun proof_result immediate (tr, proof_trs) 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

679 
let val st' = command tr st in 
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

680 
if immediate orelse null proof_trs orelse not (can proof_of st') 
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

681 
then 
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

682 
let val (results, st'') = fold_map command_result proof_trs st' 
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

683 
in (Future.value ((tr, st') :: results), st'') end 
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

684 
else 
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

685 
let 
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

686 
val (body_trs, end_tr) = split_last proof_trs; 
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

687 
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

688 

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 
val future_proof = Proof.global_future_proof 
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

690 
(fn prf => 
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

691 
Goal.fork_name "Toplevel.future_proof" 
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

692 
(fn () => 
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

693 
let val (result, result_state) = 
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

694 
(case st' of State (SOME (Proof (_, (_, orig_gthy))), prev) 
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

695 
=> State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy))), prev)) 
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

696 
> fold_map command_result body_trs > command end_tr; 
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

697 
in (result, presentation_context_of result_state) end)) 
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

698 
#> Result.put; 
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

699 

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

700 
val st'' = st' 
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

701 
> command (tr > set_print false > reset_trans > end_proof (K future_proof)); 
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

702 
val result = 
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

703 
Result.get (presentation_context_of st'') 
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

704 
> Future.map (fn body => (tr, st') :: body @ [(end_tr, st'')]); 
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

705 

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

706 
in (result, st'') end 
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

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

708 

6664  709 
end; 