author  wenzelm 
Tue, 18 Oct 2005 17:59:37 +0200  
changeset 17904  21c6894b5998 
parent 17513  0393718c2f1c 
child 18563  1df7022eac6f 
permissions  rwrr 
5828  1 
(* Title: Pure/Isar/toplevel.ML 
2 
ID: $Id$ 

3 
Author: Markus Wenzel, TU Muenchen 

4 

5 
The Isabelle/Isar toplevel. 

6 
*) 

7 

8 
signature TOPLEVEL = 

9 
sig 

16815  10 
datatype node = 
17076  11 
Theory of theory * Proof.context option  
12 
Proof of ProofHistory.T  

13 
SkipProof of int History.T * theory 

5828  14 
type state 
15 
val toplevel: state 

7732  16 
val is_toplevel: state > bool 
17076  17 
val level: state > int 
6689  18 
exception UNDEF 
17266  19 
val assert: bool > unit 
6689  20 
val node_history_of: state > node History.T 
5828  21 
val node_of: state > node 
6664  22 
val node_case: (theory > 'a) > (Proof.state > 'a) > state > 'a 
5828  23 
val theory_of: state > theory 
16452  24 
val sign_of: state > theory (*obsolete*) 
17076  25 
val body_context_of: state > Proof.context 
17208  26 
val no_body_context: state > state 
5828  27 
val proof_of: state > Proof.state 
17076  28 
val is_proof: state > bool 
9453  29 
val enter_forward_proof: state > Proof.state 
16815  30 
val prompt_state_default: state > string 
31 
val prompt_state_fn: (state > string) ref 

32 
val print_state_context: state > unit 

33 
val print_state_default: bool > state > unit 

34 
val print_state_hook: (bool > state > unit) > unit 

35 
val print_state_fn: (bool > state > unit) ref 

36 
val print_state: bool > state > unit 

37 
val pretty_state: bool > state > Pretty.T list 

16682  38 
val quiet: bool ref 
39 
val debug: bool ref 

17321
227f1f5c3959
added interact flag to control mode of excursions;
wenzelm
parents:
17320
diff
changeset

40 
val interact: bool ref 
16682  41 
val timing: bool ref 
42 
val profiling: int ref 

16815  43 
val skip_proofs: bool ref 
5828  44 
exception TERMINATE 
5990  45 
exception RESTART 
16682  46 
type transition 
6689  47 
val undo_limit: bool > int option 
5828  48 
val empty: transition 
14923  49 
val name_of: transition > string 
50 
val source_of: transition > OuterLex.token list option 

5828  51 
val name: string > transition > transition 
52 
val position: Position.T > transition > transition 

14923  53 
val source: OuterLex.token list > transition > transition 
5828  54 
val interactive: bool > transition > transition 
55 
val print: transition > transition 

16607  56 
val print': string > transition > transition 
17363  57 
val three_buffersN: string 
58 
val print3: transition > transition 

9010  59 
val no_timing: transition > transition 
5828  60 
val reset: transition > transition 
8465  61 
val init: (bool > node) > (node > unit) > (node > unit) > transition > transition 
6689  62 
val exit: transition > transition 
63 
val kill: transition > transition 

5828  64 
val keep: (state > unit) > transition > transition 
7612  65 
val keep': (bool > state > unit) > transition > transition 
6689  66 
val history: (node History.T > node History.T) > transition > transition 
5828  67 
val imperative: (unit > unit) > transition > transition 
7105  68 
val init_theory: (bool > theory) > (theory > unit) > (theory > unit) 
6689  69 
> transition > transition 
5828  70 
val theory: (theory > theory) > transition > transition 
7612  71 
val theory': (bool > theory > theory) > transition > transition 
17076  72 
val theory_context: (theory > theory * Proof.context) > transition > transition 
17363  73 
val theory_to_proof: (theory > Proof.state) > transition > transition 
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

74 
val proof: (Proof.state > Proof.state) > transition > transition 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

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

76 
val proof': (bool > Proof.state > Proof.state) > transition > transition 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

77 
val proofs': (bool > Proof.state > Proof.state Seq.seq) > transition > transition 
16815  78 
val actual_proof: (ProofHistory.T > ProofHistory.T) > transition > transition 
79 
val skip_proof: (int History.T > int History.T) > transition > transition 

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

80 
val proof_to_theory: (Proof.state > theory) > transition > transition 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

81 
val proof_to_theory': (bool > Proof.state > theory) > transition > transition 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

82 
val proof_to_theory_context: (bool > Proof.state > theory * Proof.context) 
17076  83 
> 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 
9512  85 
val unknown_theory: transition > transition 
86 
val unknown_proof: transition > transition 

87 
val unknown_context: transition > transition 

5922  88 
val exn_message: exn > string 
5828  89 
val apply: bool > transition > state > (state * (exn * string) option) option 
17266  90 
val command: transition > state > state 
17076  91 
val present_excursion: (transition * (state > state > 'a > 'a)) list > 'a > 'a 
5828  92 
val excursion: transition list > unit 
93 
val set_state: state > unit 

94 
val get_state: unit > state 

95 
val exn: unit > (exn * string) option 

96 
val >> : transition > bool 

14985  97 
val >>> : transition list > unit 
14091  98 
type 'a isar 
99 
val loop: 'a isar > unit 

5828  100 
end; 
101 

6965  102 
structure Toplevel: TOPLEVEL = 
5828  103 
struct 
104 

105 

106 
(** toplevel state **) 

107 

16815  108 
(* datatype state *) 
5828  109 

110 
datatype node = 

17076  111 
Theory of theory * Proof.context option  (*theory with optional body context*) 
112 
Proof of ProofHistory.T  (*history of proof states*) 

113 
SkipProof of int History.T * theory; (*history of proof depths*) 

5828  114 

8465  115 
datatype state = State of (node History.T * ((node > unit) * (node > unit))) option; 
5828  116 

15531  117 
val toplevel = State NONE; 
5828  118 

15531  119 
fun is_toplevel (State NONE) = true 
7732  120 
 is_toplevel _ = false; 
121 

17076  122 
fun level (State NONE) = 0 
123 
 level (State (SOME (node, _))) = 

124 
(case History.current node of 

125 
Theory _ => 0 

126 
 Proof prf => Proof.level (ProofHistory.current prf) 

127 
 SkipProof (h, _) => History.current h + 1); (*different notion of proof depth!*) 

128 

15531  129 
fun str_of_state (State NONE) = "at top level" 
16815  130 
 str_of_state (State (SOME (node, _))) = 
131 
(case History.current node of 

132 
Theory _ => "in theory mode" 

133 
 Proof _ => "in proof mode" 

134 
 SkipProof _ => "in skipped proof mode"); 

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

135 

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

136 

5828  137 
(* top node *) 
138 

6689  139 
exception UNDEF; 
140 

17266  141 
fun assert true = () 
142 
 assert false = raise UNDEF; 

143 

15531  144 
fun node_history_of (State NONE) = raise UNDEF 
145 
 node_history_of (State (SOME (node, _))) = node; 

6689  146 

147 
val node_of = History.current o node_history_of; 

5828  148 

6664  149 
fun node_case f g state = 
5828  150 
(case node_of state of 
17076  151 
Theory (thy, _) => f thy 
16815  152 
 Proof prf => g (ProofHistory.current prf) 
153 
 SkipProof (_, thy) => f thy); 

5828  154 

6664  155 
val theory_of = node_case I Proof.theory_of; 
16452  156 
val sign_of = theory_of; 
17076  157 

158 
fun body_context_of state = 

159 
(case node_of state of 

160 
Theory (_, SOME ctxt) => ctxt 

161 
 _ => node_case ProofContext.init Proof.context_of state); 

162 

17208  163 
fun no_body_context (State NONE) = State NONE 
164 
 no_body_context (State (SOME (node, x))) = 

165 
State (SOME (History.apply (fn Theory (thy, _) => Theory (thy, NONE)  nd => nd) node, x)); 

166 

6664  167 
val proof_of = node_case (fn _ => raise UNDEF) I; 
17076  168 
val is_proof = can proof_of; 
6664  169 

17363  170 
val enter_forward_proof = node_case (Proof.init o ProofContext.init) Proof.enter_forward; 
5828  171 

172 

16815  173 
(* prompt state *) 
174 

175 
fun prompt_state_default (State _) = Source.default_prompt; 

176 

177 
val prompt_state_fn = ref prompt_state_default; 

178 
fun prompt_state state = ! prompt_state_fn state; 

179 

180 

181 
(* print state *) 

182 

183 
fun pretty_context thy = [Pretty.block 

184 
[Pretty.str "theory", Pretty.brk 1, Pretty.str (Context.theory_name thy), 

185 
Pretty.str " =", Pretty.brk 1, ThyInfo.pretty_theory thy]]; 

186 

187 
fun pretty_state_context state = 

188 
(case try theory_of state of NONE => [] 

189 
 SOME thy => pretty_context thy); 

190 

17076  191 
fun pretty_node prf_only (Theory (thy, _)) = if prf_only then [] else pretty_context thy 
16815  192 
 pretty_node _ (Proof prf) = 
193 
Proof.pretty_state (ProofHistory.position prf) (ProofHistory.current prf) 

194 
 pretty_node _ (SkipProof (h, _)) = 

195 
[Pretty.str ("skipped proof: depth " ^ string_of_int (History.current h))]; 

196 

197 
fun pretty_state prf_only state = 

198 
let val ref (begin_state, end_state, _) = Display.current_goals_markers in 

199 
(case try node_of state of NONE => [] 

200 
 SOME node => 

201 
(if begin_state = "" then [] else [Pretty.str begin_state]) @ 

202 
pretty_node prf_only node @ 

203 
(if end_state = "" then [] else [Pretty.str end_state])) 

204 
end; 

205 

206 
val print_state_context = Pretty.writelns o pretty_state_context; 

207 
fun print_state_default prf_only state = Pretty.writelns (pretty_state prf_only state); 

208 

209 
val print_state_hooks = ref ([]: (bool > state > unit) list); 

210 
fun print_state_hook f = change print_state_hooks (cons f); 

211 
val print_state_fn = ref print_state_default; 

212 

213 
fun print_state prf_only state = 

214 
(List.app (fn f => (try (fn () => f prf_only state) (); ())) (! print_state_hooks); 

215 
! print_state_fn prf_only state); 

216 

217 

15668  218 

5828  219 
(** toplevel transitions **) 
220 

16682  221 
val quiet = ref false; 
222 
val debug = ref false; 

17321
227f1f5c3959
added interact flag to control mode of excursions;
wenzelm
parents:
17320
diff
changeset

223 
val interact = ref false; 
16682  224 
val timing = Output.timing; 
225 
val profiling = ref 0; 

16815  226 
val skip_proofs = ref false; 
16682  227 

5828  228 
exception TERMINATE; 
5990  229 
exception RESTART; 
7022  230 
exception EXCURSION_FAIL of exn * string; 
6689  231 
exception FAILURE of state * exn; 
5828  232 

233 

16815  234 
(* node transactions and recovery from stale theories *) 
6689  235 

16815  236 
(*NB: proof commands should be nondestructive!*) 
7022  237 

6689  238 
local 
239 

16452  240 
fun is_stale state = Context.is_stale (theory_of state) handle UNDEF => false; 
6689  241 

16815  242 
val stale_theory = ERROR_MESSAGE "Stale theory encountered after succesful execution!"; 
243 

17076  244 
fun checkpoint_node true (Theory (thy, ctxt)) = Theory (Theory.checkpoint thy, ctxt) 
6689  245 
 checkpoint_node _ node = node; 
246 

17076  247 
fun copy_node true (Theory (thy, ctxt)) = Theory (Theory.copy thy, ctxt) 
6689  248 
 copy_node _ node = node; 
249 

15531  250 
fun return (result, NONE) = result 
251 
 return (result, SOME exn) = raise FAILURE (result, exn); 

7022  252 

16729  253 
fun debug_trans f x = 
254 
if ! debug then 

16815  255 
setmp Output.transform_exceptions false 
256 
exception_trace (fn () => f x) 

16729  257 
else f x; 
258 

259 
fun interruptible f x = 

260 
let val y = ref x 

261 
in raise_interrupt (fn () => y := f x) (); ! y end; 

262 

6689  263 
in 
264 

16815  265 
fun transaction _ _ _ (State NONE) = raise UNDEF 
266 
 transaction int hist f (State (SOME (node, term))) = 

6689  267 
let 
16046
7d68cd1b1b8b
node_trans: revert to original transaction code (pre 1.54);
wenzelm
parents:
15973
diff
changeset

268 
val cont_node = History.map (checkpoint_node int) node; 
7d68cd1b1b8b
node_trans: revert to original transaction code (pre 1.54);
wenzelm
parents:
15973
diff
changeset

269 
val back_node = History.map (copy_node int) cont_node; 
16729  270 
fun state nd = State (SOME (nd, term)); 
271 
fun normal_state nd = (state nd, NONE); 

272 
fun error_state nd exn = (state nd, SOME exn); 

6689  273 

16729  274 
val (result, err) = 
275 
cont_node 

276 
> ((fn nd => f int nd) 

277 
> (if hist then History.apply_copy (copy_node int) else History.map) 

278 
> debug_trans 

279 
> interruptible 

280 
> transform_error) 

281 
> normal_state 

282 
handle exn => error_state cont_node exn; 

6689  283 
in 
16729  284 
if is_stale result 
285 
then return (error_state back_node (if_none err stale_theory)) 

286 
else return (result, err) 

6689  287 
end; 
288 

289 
end; 

290 

291 

292 
(* primitive transitions *) 

293 

16815  294 
(*NB: recovery from stale theories is provided only for theorylevel 
295 
operations via MapCurrent and AppCurrent. Other node or state 

296 
operations should not touch theories at all. 

6965  297 

16815  298 
Interrupts are enabled only for Keep, MapCurrent, and AppCurrent.*) 
5828  299 

300 
datatype trans = 

6689  301 
Reset  (*empty toplevel*) 
8465  302 
Init of (bool > node) * ((node > unit) * (node > unit))  
303 
(*init node; provide exit/kill operation*) 

304 
Exit  (*conclude node*) 

6689  305 
Kill  (*abort node*) 
7612  306 
Keep of bool > state > unit  (*peek at state*) 
6689  307 
History of node History.T > node History.T  (*history operation (undo etc.)*) 
308 
MapCurrent of bool > node > node  (*change node, bypassing history*) 

309 
AppCurrent of bool > node > node; (*change node, recording history*) 

310 

15531  311 
fun undo_limit int = if int then NONE else SOME 0; 
6689  312 

313 
local 

5828  314 

6689  315 
fun apply_tr _ Reset _ = toplevel 
15531  316 
 apply_tr int (Init (f, term)) (State NONE) = 
317 
State (SOME (History.init (undo_limit int) (f int), term)) 

318 
 apply_tr _ (Init _ ) (State (SOME _)) = raise UNDEF 

319 
 apply_tr _ Exit (State NONE) = raise UNDEF 

320 
 apply_tr _ Exit (State (SOME (node, (exit, _)))) = 

321 
(exit (History.current node); State NONE) 

322 
 apply_tr _ Kill (State NONE) = raise UNDEF 

323 
 apply_tr _ Kill (State (SOME (node, (_, kill)))) = 

324 
(kill (History.current node); State NONE) 

12987  325 
 apply_tr int (Keep f) state = (raise_interrupt (f int) state; state) 
15531  326 
 apply_tr _ (History _) (State NONE) = raise UNDEF 
327 
 apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term)) 

16815  328 
 apply_tr int (MapCurrent f) state = transaction int false f state 
329 
 apply_tr int (AppCurrent f) state = transaction int true f state; 

5828  330 

6689  331 
fun apply_union _ [] state = raise FAILURE (state, UNDEF) 
332 
 apply_union int (tr :: trs) state = 

333 
transform_error (apply_tr int tr) state 

334 
handle UNDEF => apply_union int trs state 

335 
 FAILURE (alt_state, UNDEF) => apply_union int trs alt_state 

336 
 exn as FAILURE _ => raise exn 

337 
 exn => raise FAILURE (state, exn); 

338 

339 
in 

340 

15531  341 
fun apply_trans int trs state = (apply_union int trs state, NONE) 
342 
handle FAILURE (alt_state, exn) => (alt_state, SOME exn)  exn => (state, SOME exn); 

6689  343 

344 
end; 

5828  345 

346 

347 
(* datatype transition *) 

348 

349 
datatype transition = Transition of 

16815  350 
{name: string, (*command name*) 
351 
pos: Position.T, (*source position*) 

352 
source: OuterLex.token list option, (*source text*) 

353 
int_only: bool, (*interactiveonly*) 

354 
print: string list, (*print modes (union)*) 

355 
no_timing: bool, (*suppress timing*) 

356 
trans: trans list}; (*primitive transitions (union)*) 

5828  357 

14923  358 
fun make_transition (name, pos, source, int_only, print, no_timing, trans) = 
359 
Transition {name = name, pos = pos, source = source, 

360 
int_only = int_only, print = print, no_timing = no_timing, trans = trans}; 

5828  361 

14923  362 
fun map_transition f (Transition {name, pos, source, int_only, print, no_timing, trans}) = 
363 
make_transition (f (name, pos, source, int_only, print, no_timing, trans)); 

5828  364 

16607  365 
val empty = make_transition ("<unknown>", Position.none, NONE, false, [], false, []); 
14923  366 

367 
fun name_of (Transition {name, ...}) = name; 

368 
fun source_of (Transition {source, ...}) = source; 

5828  369 

370 

371 
(* diagnostics *) 

372 

373 
fun str_of_transition (Transition {name, pos, ...}) = quote name ^ Position.str_of pos; 

374 

375 
fun command_msg msg tr = msg ^ "command " ^ str_of_transition tr; 

376 
fun at_command tr = command_msg "At " tr ^ "."; 

377 

378 
fun type_error tr state = 

6689  379 
ERROR_MESSAGE (command_msg "Illegal application of " tr ^ " " ^ str_of_state state); 
5828  380 

381 

382 
(* modify transitions *) 

383 

14923  384 
fun name nm = map_transition (fn (_, pos, source, int_only, print, no_timing, trans) => 
385 
(nm, pos, source, int_only, print, no_timing, trans)); 

5828  386 

14923  387 
fun position pos = map_transition (fn (name, _, source, int_only, print, no_timing, trans) => 
388 
(name, pos, source, int_only, print, no_timing, trans)); 

9010  389 

14923  390 
fun source src = map_transition (fn (name, pos, _, int_only, print, no_timing, trans) => 
15531  391 
(name, pos, SOME src, int_only, print, no_timing, trans)); 
5828  392 

14923  393 
fun interactive int_only = map_transition (fn (name, pos, source, _, print, no_timing, trans) => 
394 
(name, pos, source, int_only, print, no_timing, trans)); 

395 

17363  396 
val no_timing = map_transition (fn (name, pos, source, int_only, print, _, trans) => 
397 
(name, pos, source, int_only, print, true, trans)); 

398 

399 
fun add_trans tr = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) => 

400 
(name, pos, source, int_only, print, no_timing, trans @ [tr])); 

401 

16607  402 
fun print' mode = map_transition (fn (name, pos, source, int_only, print, no_timing, trans) => 
403 
(name, pos, source, int_only, insert (op =) mode print, no_timing, trans)); 

404 

405 
val print = print' ""; 

5828  406 

17363  407 
val three_buffersN = "three_buffers"; 
408 
val print3 = print' three_buffersN; 

5828  409 

410 

411 
(* build transitions *) 

412 

413 
val reset = add_trans Reset; 

6689  414 
fun init f exit kill = add_trans (Init (f, (exit, kill))); 
415 
val exit = add_trans Exit; 

416 
val kill = add_trans Kill; 

7612  417 
val keep' = add_trans o Keep; 
6689  418 
val history = add_trans o History; 
5828  419 
val map_current = add_trans o MapCurrent; 
6689  420 
val app_current = add_trans o AppCurrent; 
5828  421 

7612  422 
fun keep f = add_trans (Keep (fn _ => f)); 
5828  423 
fun imperative f = keep (fn _ => f ()); 
424 

6689  425 
fun init_theory f exit kill = 
17076  426 
init (fn int => Theory (f int, NONE)) 
427 
(fn Theory (thy, _) => exit thy  _ => raise UNDEF) 

428 
(fn Theory (thy, _) => kill thy  _ => raise UNDEF); 

5828  429 

15668  430 

431 
(* typed transitions *) 

432 

17076  433 
fun theory f = app_current (K (fn Theory (thy, _) => Theory (f thy, NONE)  _ => raise UNDEF)); 
434 
fun theory' f = app_current (fn int => 

435 
(fn Theory (thy, _) => Theory (f int thy, NONE)  _ => raise UNDEF)); 

436 

437 
fun theory_context f = 

438 
app_current (K (fn Theory (thy, _) => Theory (apsnd SOME (f thy))  _ => raise UNDEF)); 

15668  439 

15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
14985
diff
changeset

440 
fun theory_to_proof f = app_current (fn int => 
17076  441 
(fn Theory (thy, _) => 
17452
178344c74562
theory_to_proof: check theory of initial proof state, which must not be changed;
wenzelm
parents:
17434
diff
changeset

442 
let val st = f thy in 
178344c74562
theory_to_proof: check theory of initial proof state, which must not be changed;
wenzelm
parents:
17434
diff
changeset

443 
if Theory.eq_thy (thy, Proof.theory_of st) then () 
178344c74562
theory_to_proof: check theory of initial proof state, which must not be changed;
wenzelm
parents:
17434
diff
changeset

444 
else error "Theory changed at start of proof"; 
178344c74562
theory_to_proof: check theory of initial proof state, which must not be changed;
wenzelm
parents:
17434
diff
changeset

445 
if ! skip_proofs then 
178344c74562
theory_to_proof: check theory of initial proof state, which must not be changed;
wenzelm
parents:
17434
diff
changeset

446 
SkipProof (History.init (undo_limit int) 0, #1 (Proof.global_skip_proof int st)) 
178344c74562
theory_to_proof: check theory of initial proof state, which must not be changed;
wenzelm
parents:
17434
diff
changeset

447 
else Proof (ProofHistory.init (undo_limit int) st) 
178344c74562
theory_to_proof: check theory of initial proof state, which must not be changed;
wenzelm
parents:
17434
diff
changeset

448 
end 
15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
14985
diff
changeset

449 
 _ => raise UNDEF)); 
15668  450 

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

451 
fun proofs' f = map_current (fn int => 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

452 
(fn Proof prf => Proof (ProofHistory.applys (f int) prf) 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

453 
 SkipProof (h, thy) => SkipProof (History.apply I h, thy) 
16815  454 
 _ => raise UNDEF)); 
15668  455 

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

456 
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

457 
val proofs = proofs' o K; 
6689  458 
val proof = proof' o K; 
16815  459 

460 
fun actual_proof f = map_current (fn _ => 

461 
(fn Proof prf => Proof (f prf)  _ => raise UNDEF)); 

462 

463 
fun skip_proof f = map_current (fn _ => 

464 
(fn SkipProof (h, thy) => SkipProof (f h, thy)  _ => raise UNDEF)); 

15668  465 

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

466 
fun end_proof f = map_current (fn int => 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

467 
(fn Proof prf => Theory (f int (ProofHistory.current prf)) 
17076  468 
 SkipProof (h, thy) => if History.current h = 0 then Theory (thy, NONE) else raise UNDEF 
15237
250e9be7a09d
Some changes to allow skipping of proof scripts.
berghofe
parents:
14985
diff
changeset

469 
 _ => raise UNDEF)); 
15668  470 

17076  471 
fun proof_to_theory' f = end_proof (rpair NONE oo f); 
472 
fun proof_to_theory f = proof_to_theory' (K f); 

17115  473 
fun proof_to_theory_context f = end_proof (apsnd SOME oo f); 
15668  474 

16815  475 
fun skip_proof_to_theory p = map_current (fn _ => 
17904
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

476 
(fn SkipProof (h, thy) => 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

477 
if p (History.current h) then Theory (thy, NONE) 
21c6894b5998
simplified interfaces proof/proof' etc.: perform ProofHistory.apply(s)/current internally;
wenzelm
parents:
17513
diff
changeset

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

479 
 _ => raise UNDEF)); 
5828  480 

9512  481 
val unknown_theory = imperative (fn () => warning "Unknown theory context"); 
482 
val unknown_proof = imperative (fn () => warning "Unknown proof context"); 

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

484 

5828  485 

486 

487 
(** toplevel transactions **) 

488 

489 
(* print exceptions *) 

490 

15668  491 
local 
492 

493 
fun with_context f xs = 

494 
(case Context.get_context () of NONE => [] 

16452  495 
 SOME thy => map (f thy) xs); 
15668  496 

497 
fun raised name [] = "exception " ^ name ^ " raised" 

498 
 raised name [msg] = "exception " ^ name ^ " raised: " ^ msg 

499 
 raised name msgs = cat_lines (("exception " ^ name ^ " raised:") :: msgs); 

5828  500 

15668  501 
fun exn_msg _ TERMINATE = "Exit." 
502 
 exn_msg _ RESTART = "Restart." 

503 
 exn_msg _ Interrupt = "Interrupt." 

504 
 exn_msg _ ERROR = "ERROR." 

505 
 exn_msg _ (ERROR_MESSAGE msg) = msg 

17363  506 
 exn_msg detailed (EXCEPTION (exn, msg)) = cat_lines [exn_msg detailed exn, msg] 
16452  507 
 exn_msg detailed (EXCURSION_FAIL (exn, msg)) = cat_lines [exn_msg detailed exn, msg] 
15668  508 
 exn_msg false (THEORY (msg, _)) = msg 
16452  509 
 exn_msg true (THEORY (msg, thys)) = raised "THEORY" (msg :: map Context.str_of_thy thys) 
15668  510 
 exn_msg _ (ProofContext.CONTEXT (msg, _)) = msg 
511 
 exn_msg _ (Proof.STATE (msg, _)) = msg 

512 
 exn_msg _ (ProofHistory.FAIL msg) = msg 

513 
 exn_msg detailed (MetaSimplifier.SIMPROC_FAIL (name, exn)) = 

514 
fail_msg detailed "simproc" ((name, Position.none), exn) 

515 
 exn_msg detailed (Attrib.ATTRIB_FAIL info) = fail_msg detailed "attribute" info 

516 
 exn_msg detailed (Method.METHOD_FAIL info) = fail_msg detailed "method" info 

517 
 exn_msg detailed (Antiquote.ANTIQUOTE_FAIL info) = fail_msg detailed "antiquotation" info 

518 
 exn_msg false (Syntax.AST (msg, _)) = raised "AST" [msg] 

519 
 exn_msg true (Syntax.AST (msg, asts)) = 

520 
raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts) 

521 
 exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg] 

522 
 exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg :: 

523 
with_context Sign.string_of_typ Ts @ with_context Sign.string_of_term ts) 

524 
 exn_msg false (TERM (msg, _)) = raised "TERM" [msg] 

525 
 exn_msg true (TERM (msg, ts)) = raised "TERM" (msg :: with_context Sign.string_of_term ts) 

526 
 exn_msg false (THM (msg, _, _)) = raised "THM" [msg] 

527 
 exn_msg true (THM (msg, i, thms)) = 

528 
raised ("THM " ^ string_of_int i) (msg :: map Display.string_of_thm thms) 

529 
 exn_msg _ Option = raised "Option" [] 

530 
 exn_msg _ UnequalLengths = raised "UnequalLengths" [] 

531 
 exn_msg _ Empty = raised "Empty" [] 

532 
 exn_msg _ Subscript = raised "Subscript" [] 

16197  533 
 exn_msg _ (Fail msg) = raised "Fail" [msg] 
15668  534 
 exn_msg _ exn = General.exnMessage exn 
535 
and fail_msg detailed kind ((name, pos), exn) = 

536 
"Error in " ^ kind ^ " " ^ quote name ^ Position.str_of pos ^ ":\n" ^ exn_msg detailed exn; 

15519  537 

15668  538 
in 
539 

540 
fun exn_message exn = exn_msg (! debug) exn; 

5828  541 

15531  542 
fun print_exn NONE = () 
543 
 print_exn (SOME (exn, s)) = error_msg (cat_lines [exn_message exn, s]); 

5828  544 

15668  545 
end; 
546 

5828  547 

548 
(* apply transitions *) 

549 

6664  550 
local 
551 

9010  552 
fun app int (tr as Transition {trans, int_only, print, no_timing, ...}) state = 
5828  553 
let 
16682  554 
val _ = conditional (not int andalso int_only) (fn () => 
555 
warning (command_msg "Interactiveonly " tr)); 

556 

557 
fun do_timing f x = (info (command_msg "" tr); timeap f x); 

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

559 

6689  560 
val (result, opt_exn) = 
16729  561 
state > (apply_trans int trans 
562 
> (if ! profiling > 0 then do_profiling else I) 

563 
> (if ! profiling > 0 orelse ! timing andalso not no_timing then do_timing else I)); 

16607  564 
val _ = conditional (int andalso not (! quiet) andalso 
565 
exists (fn m => m mem_string print) ("" :: ! print_mode)) 

566 
(fn () => print_state false result); 

15570  567 
in (result, Option.map (fn UNDEF => type_error tr state  exn => exn) opt_exn) end; 
6664  568 

569 
in 

5828  570 

6689  571 
fun apply int tr st = 
6965  572 
(case app int tr st of 
15531  573 
(_, SOME TERMINATE) => NONE 
574 
 (_, SOME RESTART) => SOME (toplevel, NONE) 

575 
 (state', SOME (EXCURSION_FAIL exn_info)) => SOME (state', SOME exn_info) 

576 
 (state', SOME exn) => SOME (state', SOME (exn, at_command tr)) 

577 
 (state', NONE) => SOME (state', NONE)); 

6664  578 

17266  579 
fun command tr st = 
580 
(case apply false tr st of 

581 
SOME (st', NONE) => st' 

582 
 SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info 

583 
 NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); 

584 

6664  585 
end; 
5828  586 

587 

17076  588 
(* excursion: toplevel  apply transformers/presentation  toplevel *) 
5828  589 

6664  590 
local 
591 

5828  592 
fun excur [] x = x 
17076  593 
 excur ((tr, pr) :: trs) (st, res) = 
17321
227f1f5c3959
added interact flag to control mode of excursions;
wenzelm
parents:
17320
diff
changeset

594 
(case apply (! interact) tr st of 
15531  595 
SOME (st', NONE) => 
17076  596 
excur trs (st', transform_error (fn () => pr st st' res) () handle exn => 
10324  597 
raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr)) 
15531  598 
 SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info 
599 
 NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); 

5828  600 

17076  601 
fun no_pr _ _ _ = (); 
602 

6664  603 
in 
604 

17076  605 
fun present_excursion trs res = 
15531  606 
(case excur trs (State NONE, res) of 
607 
(State NONE, res') => res' 

9134  608 
 _ => raise ERROR_MESSAGE "Unfinished development at end of input") 
609 
handle exn => error (exn_message exn); 

610 

17076  611 
fun excursion trs = present_excursion (map (rpair no_pr) trs) (); 
7062  612 

6664  613 
end; 
614 

5828  615 

616 

617 
(** interactive transformations **) 

618 

619 
(* the global state reference *) 

620 

15531  621 
val global_state = ref (toplevel, NONE: (exn * string) option); 
5828  622 

15531  623 
fun set_state state = global_state := (state, NONE); 
5828  624 
fun get_state () = fst (! global_state); 
625 
fun exn () = snd (! global_state); 

626 

627 

6965  628 
(* the Isar source of transitions *) 
629 

14091  630 
type 'a isar = 
6965  631 
(transition, (transition option, 
12881  632 
(OuterLex.token, (OuterLex.token option, (OuterLex.token, (OuterLex.token, 
14091  633 
Position.T * (Symbol.symbol, (string, 'a) Source.source) Source.source) 
12881  634 
Source.source) Source.source) Source.source) Source.source) Source.source) Source.source; 
6965  635 

636 

5828  637 
(* apply transformers to global state *) 
638 

14985  639 
nonfix >> >>>; 
5828  640 

641 
fun >> tr = 

642 
(case apply true tr (get_state ()) of 

15531  643 
NONE => false 
644 
 SOME (state', exn_info) => 

5828  645 
(global_state := (state', exn_info); 
16729  646 
print_exn exn_info; 
5828  647 
true)); 
648 

14985  649 
fun >>> [] = () 
650 
 >>> (tr :: trs) = if >> tr then >>> trs else (); 

651 

17513
0393718c2f1c
get_interrupt: special handling of IO.io now in MLSystems/smlnjbasiscompat.ML;
wenzelm
parents:
17500
diff
changeset

652 
(*Spurious interrupts ahead! Race condition?*) 
0393718c2f1c
get_interrupt: special handling of IO.io now in MLSystems/smlnjbasiscompat.ML;
wenzelm
parents:
17500
diff
changeset

653 
fun get_interrupt src = SOME (Source.get_single src) handle Interrupt => NONE; 
7602  654 

5828  655 
fun raw_loop src = 
7602  656 
(case get_interrupt (Source.set_prompt (prompt_state (get_state ())) src) of 
15531  657 
NONE => (writeln "\nInterrupt."; raw_loop src) 
658 
 SOME NONE => () 

659 
 SOME (SOME (tr, src')) => if >> tr then raw_loop src' else ()); 

5828  660 

12987  661 
fun loop src = ignore_interrupt raw_loop src; 
5828  662 

663 
end; 