337 | apply_tr _ Exit (State (SOME (node, (exit, _)))) = |
337 | apply_tr _ Exit (State (SOME (node, (exit, _)))) = |
338 (exit (History.current node); State NONE) |
338 (exit (History.current node); State NONE) |
339 | apply_tr _ Kill (State NONE) = raise UNDEF |
339 | apply_tr _ Kill (State NONE) = raise UNDEF |
340 | apply_tr _ Kill (State (SOME (node, (_, kill)))) = |
340 | apply_tr _ Kill (State (SOME (node, (_, kill)))) = |
341 (kill (History.current node); State NONE) |
341 (kill (History.current node); State NONE) |
342 | apply_tr int (Keep f) state = (raise_interrupt (f int) state; state) |
342 | apply_tr int (Keep f) state = |
|
343 (setmp Output.do_toplevel_errors false (raise_interrupt (f int)) state; state) |
343 | apply_tr _ (History _) (State NONE) = raise UNDEF |
344 | apply_tr _ (History _) (State NONE) = raise UNDEF |
344 | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term)) |
345 | apply_tr _ (History f) (State (SOME (node, term))) = State (SOME (f node, term)) |
345 | apply_tr int (Transaction (hist, f)) state = transaction hist (fn x => f int x) state; |
346 | apply_tr int (Transaction (hist, f)) state = transaction hist (fn x => f int x) state; |
346 |
347 |
347 fun apply_union _ [] state = raise FAILURE (state, UNDEF) |
348 fun apply_union _ [] state = raise FAILURE (state, UNDEF) |
627 fun excursion trs = present_excursion (map (rpair no_pr) trs) (); |
628 fun excursion trs = present_excursion (map (rpair no_pr) trs) (); |
628 |
629 |
629 end; |
630 end; |
630 |
631 |
631 |
632 |
632 (* program: independent of state *) |
633 (* toplevel program: independent of state *) |
633 |
634 |
634 fun program f = |
635 fun program f = |
635 ((fn () => debugging f () handle exn => error (exn_message exn)) |
636 Output.ML_errors (fn () => debugging f () handle exn => error (exn_message exn)) (); |
636 |> setmp Output.do_toplevel_errors true |
|
637 |> Output.toplevel_errors) (); |
|
638 |
637 |
639 |
638 |
640 |
639 |
641 (** interactive transformations **) |
640 (** interactive transformations **) |
642 |
641 |