author  wenzelm 
Tue, 20 Jul 2010 20:56:28 +0200  
changeset 37858  e1ef6b441fe7 
parent 37856  173974e07dea 
child 37859  575a14dd4167 
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 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

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

12 
val toplevel: state 
7732  13 
val is_toplevel: state > bool 
18589  14 
val is_theory: state > bool 
15 
val is_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 
21007  24 
val enter_proof_body: state > Proof.state 
16815  25 
val print_state_context: state > unit 
26 
val print_state: bool > state > unit 

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

30 
val interact: bool Unsynchronized.ref 

31 
val timing: bool Unsynchronized.ref 

32 
val profiling: int Unsynchronized.ref 

33 
val skip_proofs: bool Unsynchronized.ref 

5828  34 
exception TERMINATE 
27583  35 
exception TOPLEVEL_ERROR 
20128
8f0e07d7cf92
keep/transaction: unified execution model (with debugging etc.);
wenzelm
parents:
19996
diff
changeset

36 
val program: (unit > 'a) > 'a 
33604
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

37 
val thread: bool > (unit > unit) > Thread.thread 
16682  38 
type transition 
5828  39 
val empty: transition 
27441  40 
val init_of: transition > string option 
27427  41 
val name_of: transition > string 
28105  42 
val pos_of: transition > Position.T 
27500  43 
val str_of: transition > string 
5828  44 
val name: string > transition > transition 
45 
val position: Position.T > transition > transition 

46 
val interactive: bool > transition > transition 

47 
val print: transition > transition 

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

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

5828  56 
val theory: (theory > theory) > transition > transition 
26491  57 
val generic_theory: (generic_theory > generic_theory) > transition > transition 
7612  58 
val theory': (bool > theory > theory) > transition > transition 
20985  59 
val begin_local_theory: bool > (theory > local_theory) > transition > transition 
21007  60 
val end_local_theory: transition > transition 
29380  61 
val local_theory': xstring option > (bool > local_theory > local_theory) > 
62 
transition > transition 

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

63 
val local_theory: xstring option > (local_theory > local_theory) > transition > transition 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

64 
val present_local_theory: xstring option > (state > unit) > transition > transition 
24453  65 
val local_theory_to_proof': xstring option > (bool > local_theory > Proof.state) > 
66 
transition > transition 

21007  67 
val local_theory_to_proof: xstring option > (local_theory > Proof.state) > 
68 
transition > transition 

17363  69 
val theory_to_proof: (theory > Proof.state) > transition > transition 
21007  70 
val end_proof: (bool > Proof.state > Proof.context) > transition > transition 
71 
val forget_proof: transition > transition 

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

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

74 
val proof': (bool > Proof.state > Proof.state) > transition > transition 
21177  75 
val proofs: (Proof.state > Proof.state Seq.seq) > transition > transition 
76 
val proof: (Proof.state > Proof.state) > transition > transition 

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

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

79 
val skip_proof_to_theory: (int > bool) > transition > transition 
27427  80 
val get_id: transition > string option 
81 
val put_id: string > transition > transition 

9512  82 
val unknown_theory: transition > transition 
83 
val unknown_proof: transition > transition 

84 
val unknown_context: transition > transition 

28425  85 
val setmp_thread_position: transition > ('a > 'b) > 'a > 'b 
27606  86 
val status: transition > Markup.T > unit 
26602
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

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

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

89 
val transition: bool > transition > state > (state * (exn * string) option) option 
37687
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

90 
val run_command: string > transition > state > state option 
28425  91 
val commit_exit: Position.T > transition 
92 
val command: transition > state > state 

29427
7ba952481e29
excursion: commit_exit internally  checkpoints are fully persistent now;
wenzelm
parents:
29386
diff
changeset

93 
val excursion: (transition * transition list) list > (transition * state) list lazy 
5828  94 
end; 
95 

6965  96 
structure Toplevel: TOPLEVEL = 
5828  97 
struct 
98 

99 
(** toplevel state **) 

100 

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

101 
exception UNDEF = Runtime.UNDEF; 
19063  102 

103 

21294  104 
(* local theory wrappers *) 
5828  105 

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

106 
type generic_theory = Context.generic; (*theory or local_theory*) 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

107 

35205  108 
val loc_init = Theory_Target.context_cmd; 
33671  109 
val loc_exit = Local_Theory.exit_global; 
21294  110 

25292  111 
fun loc_begin loc (Context.Theory thy) = loc_init (the_default "" loc) thy 
21294  112 
 loc_begin NONE (Context.Proof lthy) = lthy 
25269  113 
 loc_begin (SOME loc) (Context.Proof lthy) = loc_init loc (loc_exit lthy); 
21294  114 

115 
fun loc_finish _ (Context.Theory _) = Context.Theory o loc_exit 

33671  116 
 loc_finish NONE (Context.Proof _) = Context.Proof o Local_Theory.restore 
25292  117 
 loc_finish (SOME _) (Context.Proof lthy) = fn lthy' => 
33671  118 
Context.Proof (Local_Theory.reinit (Local_Theory.raw_theory (K (loc_exit lthy')) 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 

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

143 
type node_info = node * (theory > unit); (*node with exit operation*) 
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

144 
datatype state = State of node_info option * node_info option; (*current, previous*) 
5828  145 

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

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

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

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

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

151 
fun level (State (NONE, _)) = 0 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

152 
 level (State (SOME (Theory _, _), _)) = 0 
33390  153 
 level (State (SOME (Proof (prf, _), _), _)) = Proof.level (Proof_Node.current prf) 
27576
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

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

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

156 
fun str_of_state (State (NONE, _)) = "at top level" 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

157 
 str_of_state (State (SOME (Theory (Context.Theory _, _), _), _)) = "in theory mode" 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

158 
 str_of_state (State (SOME (Theory (Context.Proof _, _), _), _)) = "in local theory mode" 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

159 
 str_of_state (State (SOME (Proof _, _), _)) = "in proof mode" 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

160 
 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

161 

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

162 

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

163 
(* current node *) 
5828  164 

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

165 
fun node_of (State (NONE, _)) = raise UNDEF 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

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

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

170 

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

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

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

176 
 SOME node => context_node node 

177 
 NONE => raise UNDEF); 

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

178 

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

181 

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

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

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

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

21007  192 
val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward; 
5828  193 

194 

16815  195 
(* print state *) 
196 

33671  197 
val pretty_context = Local_Theory.pretty o Context.cases (Theory_Target.init NONE) I; 
16815  198 

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

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

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

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

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

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

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

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

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

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

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

33390  212 
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

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

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

16815  218 

15668  219 

5828  220 
(** toplevel transitions **) 
221 

32738  222 
val quiet = Unsynchronized.ref false; 
22135  223 
val debug = Output.debugging; 
32738  224 
val interact = Unsynchronized.ref false; 
16682  225 
val timing = Output.timing; 
32738  226 
val profiling = Unsynchronized.ref 0; 
227 
val skip_proofs = Unsynchronized.ref false; 

16682  228 

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

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

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

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

232 

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

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

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

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

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

237 

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

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

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

240 
(((fn () => body () handle Exn.Interrupt => ()) 
d4220df6fde2
Toplevel.thread provides Isarstyle exception output;
wenzelm
parents:
33553
diff
changeset

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

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

243 
(fn exn => priority ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))), 
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
37208
diff
changeset

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

245 

5828  246 

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

247 
(* node transactions  maintaining stable checkpoints *) 
7022  248 

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

249 
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

250 

6689  251 
local 
252 

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

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

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

255 

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

256 
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

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

258 

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

259 
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

260 

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

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

262 
 stale_error some = some; 
16815  263 

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

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

266 
 map_theory _ node = node; 
6689  267 

268 
in 

269 

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

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

272 
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

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

274 
val back_node = map_theory (Theory.checkpoint o Theory.copy) cont_node; 
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

275 
fun state_error e nd = (State (SOME (nd, exit), SOME (node, exit)), e); 
6689  276 

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

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

278 
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

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

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

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

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

283 

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

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

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

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

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

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

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

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

291 
end; 
6689  292 

293 
end; 

294 

295 

296 
(* primitive transitions *) 

297 

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

299 
Init of string * (bool > theory) * (theory > unit)  (*theory name, init, exit*) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

300 
Exit  (*formal exit of theory  without committing*) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

301 
CommitExit  (*exit and commit final theory*) 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

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

303 
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

304 

6689  305 
local 
5828  306 

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

308 
State (SOME (Theory (Context.Theory 
e2d5d7f51aa3
init_theory: Runtime.controlled_execution for proper exception trace etc.;
wenzelm
parents:
33725
diff
changeset

309 
(Theory.checkpoint (Runtime.controlled_execution f int)), NONE), exit), NONE) 
32792  310 
 apply_tr _ Exit (State (prev as SOME (Theory (Context.Theory _, _), _), _)) = 
27603  311 
State (NONE, prev) 
32792  312 
 apply_tr _ CommitExit (State (NONE, SOME (Theory (Context.Theory thy, _), exit))) = 
31476
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset

313 
(Runtime.controlled_execution exit thy; toplevel) 
32792  314 
 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

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

318 
 apply_tr _ _ _ = raise UNDEF; 

5828  319 

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

322 
apply_union int trs state 

323 
handle Runtime.UNDEF => apply_tr int tr state 

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

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

327 

328 
in 

329 

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

333 
end; 

5828  334 

335 

336 
(* datatype transition *) 

337 

338 
datatype transition = Transition of 

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

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

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

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

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

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

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

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

346 
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

347 
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

348 
trans = trans}; 
5828  349 

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

350 
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

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

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

355 

356 
(* diagnostics *) 

357 

27441  358 
fun init_of (Transition {trans = [Init (name, _, _)], ...}) = SOME name 
359 
 init_of _ = NONE; 

360 

27427  361 
fun name_of (Transition {name, ...}) = name; 
28105  362 
fun pos_of (Transition {pos, ...}) = pos; 
363 
fun str_of tr = quote (name_of tr) ^ Position.str_of (pos_of tr); 

5828  364 

27427  365 
fun command_msg msg tr = msg ^ "command " ^ str_of tr; 
5828  366 
fun at_command tr = command_msg "At " tr ^ "."; 
367 

368 
fun type_error tr state = 

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

371 

372 
(* modify transitions *) 

373 

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

374 
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

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

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

377 
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

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

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

380 
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

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

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

383 
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

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

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

386 
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

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

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

389 
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

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

391 

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

392 
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

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

394 

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

395 
val print = set_print true; 
5828  396 

397 

21007  398 
(* basic transitions *) 
5828  399 

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

400 
fun init_theory name f exit = add_trans (Init (name, f, exit)); 
6689  401 
val exit = add_trans Exit; 
7612  402 
val keep' = add_trans o Keep; 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

403 

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

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

405 
fun transaction f = present_transaction f (K ()); 
5828  406 

7612  407 
fun keep f = add_trans (Keep (fn _ => f)); 
5828  408 
fun imperative f = keep (fn _ => f ()); 
409 

27840  410 
fun ignored pos = empty > name "<ignored>" > position pos > imperative I; 
411 
fun malformed pos msg = 

412 
empty > name "<malformed>" > position pos > imperative (fn () => error msg); 

413 

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

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

15668  417 

21007  418 

419 
(* theory transitions *) 

15668  420 

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

421 
fun generic_theory f = transaction (fn _ => 
26491  422 
(fn Theory (gthy, _) => Theory (f gthy, NONE) 
423 
 _ => raise UNDEF)); 

424 

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

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

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

427 
let val thy' = thy 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

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

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

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

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

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

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

434 

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

435 
fun theory f = theory' (K f); 
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
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 begin_local_theory begin f = transaction (fn _ => 
20963
a7fd8f05a2be
added type global_theory  theory or local_theory;
wenzelm
parents:
20928
diff
changeset

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

439 
let 
20985  440 
val lthy = f thy; 
21294  441 
val gthy = if begin then Context.Proof lthy else Context.Theory (loc_exit lthy); 
442 
in Theory (gthy, SOME lthy) end 

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

443 
 _ => raise UNDEF)); 
17076  444 

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

445 
val end_local_theory = transaction (fn _ => 
21294  446 
(fn Theory (Context.Proof lthy, _) => Theory (Context.Theory (loc_exit lthy), SOME lthy) 
21007  447 
 _ => raise UNDEF)); 
448 

449 
local 

450 

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

451 
fun local_theory_presentation loc f = present_transaction (fn int => 
21294  452 
(fn Theory (gthy, _) => 
453 
let 

454 
val finish = loc_finish loc gthy; 

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

455 
val lthy' = loc_begin loc gthy 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

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

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

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

460 
 _ => raise UNDEF)); 
15668  461 

21007  462 
in 
463 

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

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

466 
fun present_local_theory loc = local_theory_presentation loc (K I); 
18955  467 

21007  468 
end; 
469 

470 

471 
(* proof transitions *) 

472 

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

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

474 
(fn Proof (prf, (finish, _)) => 
33390  475 
let val state = Proof_Node.current prf in 
21007  476 
if can (Proof.assert_bottom true) state then 
477 
let 

478 
val ctxt' = f int state; 

479 
val gthy' = finish ctxt'; 

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

481 
else raise UNDEF 

482 
end 

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

483 
 SkipProof (0, (gthy, _)) => Theory (gthy, NONE) 
21007  484 
 _ => raise UNDEF)); 
485 

21294  486 
local 
487 

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

488 
fun begin_proof init finish = transaction (fn int => 
21294  489 
(fn Theory (gthy, _) => 
490 
let 

24453  491 
val prf = init int gthy; 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

492 
val skip = ! skip_proofs; 
21294  493 
val schematic = Proof.schematic_goal prf; 
494 
in 

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

495 
if skip andalso schematic then 
21294  496 
warning "Cannot skip proof of schematic goal statement" 
497 
else (); 

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

498 
if skip andalso not schematic then 
27564
fc6d34e49e17
replaced obsolete ProofHistory by ProofNode (backtracking only);
wenzelm
parents:
27500
diff
changeset

499 
SkipProof (0, (finish gthy (Proof.global_skip_proof int prf), gthy)) 
33390  500 
else Proof (Proof_Node.init prf, (finish gthy, gthy)) 
21294  501 
end 
502 
 _ => raise UNDEF)); 

503 

504 
in 

505 

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

506 
fun local_theory_to_proof' loc f = begin_proof 
33725
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

507 
(fn int => fn gthy => f int (Local_Theory.new_group (loc_begin loc gthy))) 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

508 
(fn gthy => loc_finish loc gthy o Local_Theory.reset_group); 
24780
47bb1e380d83
local_theory transactions: more careful treatment of context position;
wenzelm
parents:
24634
diff
changeset

509 

24453  510 
fun local_theory_to_proof loc f = local_theory_to_proof' loc (K f); 
21294  511 

512 
fun theory_to_proof f = begin_proof 

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

513 
(K (fn Context.Theory thy => f (Theory.checkpoint (Sign.new_group thy))  _ => raise UNDEF)) 
a8481da77270
implicit name space grouping for theory/local_theory transactions;
wenzelm
parents:
33671
diff
changeset

514 
(K (Context.Theory o Sign.reset_group o ProofContext.theory_of)); 
21294  515 

516 
end; 

517 

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

518 
val forget_proof = transaction (fn _ => 
21007  519 
(fn Proof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 
520 
 SkipProof (_, (_, orig_gthy)) => Theory (orig_gthy, NONE) 

521 
 _ => raise UNDEF)); 

522 

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

523 
val present_proof = present_transaction (fn _ => 
33390  524 
(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

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

526 
 _ => raise UNDEF)); 
21177  527 

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

528 
fun proofs' f = transaction (fn int => 
33390  529 
(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

530 
 skip as SkipProof _ => skip 
16815  531 
 _ => raise UNDEF)); 
15668  532 

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

533 
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

534 
val proofs = proofs' o K; 
6689  535 
val proof = proof' o K; 
16815  536 

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

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

539 
 _ => raise UNDEF)); 
16815  540 

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

541 
fun skip_proof f = transaction (fn _ => 
21007  542 
(fn SkipProof (h, x) => SkipProof (f h, x) 
18563  543 
 _ => raise UNDEF)); 
544 

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

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

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

547 
 _ => raise UNDEF)); 
5828  548 

549 

550 

551 
(** toplevel transactions **) 

552 

27427  553 
(* identification *) 
554 

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

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

557 

558 

25960  559 
(* thread position *) 
25799  560 

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

562 
Position.setmp_thread_data pos f x; 
25799  563 

27606  564 
fun status tr m = 
565 
setmp_thread_position tr (fn () => Output.status (Markup.markup m "")) (); 

566 

37688  567 
fun async_state (tr as Transition {print, ...}) st = 
568 
if print then 

37711
f1ea60bb7754
async_state: report within proper transaction context;
wenzelm
parents:
37690
diff
changeset

569 
ignore 
f1ea60bb7754
async_state: report within proper transaction context;
wenzelm
parents:
37690
diff
changeset

570 
(Future.fork_group (Task_Queue.new_group (Future.worker_group ())) 
f1ea60bb7754
async_state: report within proper transaction context;
wenzelm
parents:
37690
diff
changeset

571 
(fn () => 
f1ea60bb7754
async_state: report within proper transaction context;
wenzelm
parents:
37690
diff
changeset

572 
setmp_thread_position tr (fn () => Future.report (fn () => print_state false st)) ())) 
37688  573 
else (); 
37687
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

574 

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

575 
fun error_msg tr 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

576 
setmp_thread_position tr (fn () => 
c5d2899b6de9
moved Isar toplevel runtime support to runtime.ML, which is loaded early (before ml_compiler.ML);
wenzelm
parents:
31431
diff
changeset

577 
Output.error_msg (ML_Compiler.exn_message (EXCURSION_FAIL exn_info))) (); 
26602
5534b6a6b810
made purely valueoriented, moved global state to structure Isar (cf. isar.ML);
wenzelm
parents:
26491
diff
changeset

578 

25799  579 

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

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

581 

32738  582 
local val hooks = Unsynchronized.ref ([]: (transition > state > state > unit) list) in 
28095
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

583 

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

586 

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

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

588 

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

589 

5828  590 
(* apply transitions *) 
591 

6664  592 
local 
593 

32792  594 
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

595 
setmp_thread_position tr (fn state => 
25799  596 
let 
597 
fun do_timing f x = (warning (command_msg "" tr); timeap f x); 

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

599 

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

600 
val (result, status) = 
32792  601 
state > (apply_trans int trans 
25799  602 
> (if ! profiling > 0 andalso not no_timing then do_profiling else I) 
603 
> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I)); 

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

604 

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

605 
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

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

608 
in 

5828  609 

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

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

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

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

613 
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

614 

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

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

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

617 
(case app int tr st of 
7eaf0813bdc3
added add_hook interface for posttransition hooks;
wenzelm
parents:
27859
diff
changeset

618 
(_, SOME TERMINATE) => NONE 
28103
b79e61861f0f
simplified Toplevel.add_hook: cover successful transactions only;
wenzelm
parents:
28095
diff
changeset

619 
 (st', SOME (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

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

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

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

623 
in res end; 
6664  624 

625 
end; 

5828  626 

627 

37687
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

628 
(* managed execution *) 
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

629 

e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

630 
fun run_command thy_name (tr as Transition {print, ...}) st = 
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

631 
(case 
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

632 
(case init_of tr of 
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

633 
SOME name => Exn.capture (fn () => Thy_Load.check_name thy_name name) () 
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

634 
 NONE => Exn.Result ()) of 
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

635 
Exn.Result () => 
37856
173974e07dea
Topelevel.run_command: interactive mode for initial 'theory' ensures that Thy_Info.begin_theory loads parent theories;
wenzelm
parents:
37852
diff
changeset

636 
(case transition (is_some (init_of tr)) tr st of 
37687
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

637 
SOME (st', NONE) => (status tr Markup.finished; async_state tr st'; SOME st') 
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

638 
 SOME (_, SOME (exn as Exn.Interrupt, _)) => reraise exn 
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

639 
 SOME (_, SOME exn_info) => (error_msg tr exn_info; status tr Markup.failed; NONE) 
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

640 
 NONE => (error_msg tr (TERMINATE, at_command tr); status tr Markup.failed; NONE)) 
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

641 
 Exn.Exn exn => (error_msg tr (exn, at_command tr); status tr Markup.failed; NONE)); 
e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

642 

e07dacec79e7
Toplevel.run_command: asynchronous state output, as an attempt to address potentially slow pretty printing (e.g. in HOL/Bali);
wenzelm
parents:
37216
diff
changeset

643 

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

644 
(* commit final exit *) 
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

645 

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

647 
name "end" empty 
28425  648 
> position pos 
27601
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

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

650 
> imperative (fn () => warning "Expected to find finished theory"); 
6683cdb94af8
simplified commit_exit: operate on previous node of final state, include warning here;
wenzelm
parents:
27583
diff
changeset

651 

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

652 

28425  653 
(* nested commands *) 
5828  654 

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

656 
(case transition (! interact) tr st of 
28425  657 
SOME (st', NONE) => st' 
658 
 SOME (_, SOME exn_info) => raise EXCURSION_FAIL exn_info 

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

659 
 NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); 
7afff36043e6
eliminated internal command history  superceeded by global Isar state (cf. isar.ML);
wenzelm
parents:
27564
diff
changeset

660 

29483  661 
fun command_result tr st = 
662 
let val st' = command tr st 

663 
in (st', st') end; 

664 

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

665 

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

666 
(* excursion of units, consisting of commands with proof *) 
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

667 

33519  668 
structure States = 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

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

670 
type T = state list future option; 
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

671 
fun init _ = NONE; 
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 
); 
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

673 

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

674 
fun proof_result immediate (tr, proof_trs) st = 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

675 
let val st' = command tr st in 
36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
35205
diff
changeset

676 
if immediate orelse 
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
35205
diff
changeset

677 
null proof_trs orelse 
36950  678 
Keyword.is_schematic_goal (name_of tr) orelse 
679 
exists (Keyword.is_qed_global o name_of) proof_trs orelse 

36315
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
35205
diff
changeset

680 
not (can proof_of st') orelse 
e859879079c8
added keyword category "schematic goal", which prevents any attempt to fork the proof;
wenzelm
parents:
35205
diff
changeset

681 
Proof.is_relevant (proof_of st') 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

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

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

684 
in (Lazy.value ((tr, st') :: (proof_trs ~~ states)), st'') end 
28453
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

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

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

687 
val (body_trs, end_tr) = split_last proof_trs; 
28453
06702e7acd1d
excursion/unit_result: no print for forked end, finish into global theory, pick resul from presentation context;
wenzelm
parents:
28451
diff
changeset

688 
val finish = Context.Theory o ProofContext.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

689 

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

691 
(fn prf => 
32062
457f5bcd3d76
Proof.future_proof: declare all assumptions as well;
wenzelm
parents:
32058
diff
changeset

692 
Future.fork_pri ~1 (fn () => 
30366
e3d788b9dffb
simplified presentation: built into transaction, pass state directly;
wenzelm
parents:
29516
diff
changeset

693 
let val (states, 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

694 
(case st' of State (SOME (Proof (_, (_, orig_gthy)), exit), prev) 
33390  695 
=> State (SOME (Proof (Proof_Node.init prf, (finish, orig_gthy)), exit), prev)) 
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

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

697 
> command (end_tr > set_print false); 
30398  698 
in (states, presentation_context_of result_state) end)) 
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 
#> (fn (states, ctxt) => States.put (SOME states) ctxt); 
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

700 

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

701 
val st'' = st' > command (end_tr > reset_trans > end_proof (K future_proof)); 
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

702 

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 
val states = 
30398  704 
(case States.get (presentation_context_of st'') of 
37852
a902f158b4fc
eliminated oldstyle sys_error/SYS_ERROR in favour of exception Fail  after careful checking that there is no overlap with existing handling of that;
wenzelm
parents:
37711
diff
changeset

705 
NONE => raise Fail ("No future states for " ^ name_of tr ^ Position.str_of (pos_of tr)) 
28974
d6b190efa01a
excursion: pass explicit proof states as result of future proof, replaced lowlevel Thm.join_futures by PureThy.force_proofs;
wenzelm
parents:
28645
diff
changeset

706 
 SOME states => states); 
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

707 
val result = Lazy.lazy 
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

708 
(fn () => (tr, st') :: (body_trs ~~ Future.join states) @ [(end_tr, st'')]); 
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

709 

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

710 
in (result, st'') end 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

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

712 

29068  713 
fun excursion input = 
28425  714 
let 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

715 
val end_pos = if null input then error "No input" else pos_of (fst (List.last input)); 
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

716 

29448
34b9652b2f45
added Goal.future_enabled abstraction  now also checks that this is already
wenzelm
parents:
29435
diff
changeset

717 
val immediate = not (Goal.future_enabled ()); 
29427
7ba952481e29
excursion: commit_exit internally  checkpoints are fully persistent now;
wenzelm
parents:
29386
diff
changeset

718 
val (results, end_state) = fold_map (proof_result immediate) input toplevel; 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

719 
val _ = 
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

720 
(case end_state of 
29427
7ba952481e29
excursion: commit_exit internally  checkpoints are fully persistent now;
wenzelm
parents:
29386
diff
changeset

721 
State (NONE, SOME (Theory (Context.Theory _, _), _)) => 
7ba952481e29
excursion: commit_exit internally  checkpoints are fully persistent now;
wenzelm
parents:
29386
diff
changeset

722 
command (commit_exit end_pos) end_state 
28433
b3dab95f098f
begin_proof: avoid race condition wrt. skip_proofs flag;
wenzelm
parents:
28425
diff
changeset

723 
 _ => error "Unfinished development at end of input"); 
29427
7ba952481e29
excursion: commit_exit internally  checkpoints are fully persistent now;
wenzelm
parents:
29386
diff
changeset

724 
in Lazy.lazy (fn () => maps Lazy.force results) end; 
7062  725 

6664  726 
end; 