equal
deleted
inserted
replaced
572 |
572 |
573 local |
573 local |
574 |
574 |
575 fun excur [] x = x |
575 fun excur [] x = x |
576 | excur ((tr, pr) :: trs) (st, res) = |
576 | excur ((tr, pr) :: trs) (st, res) = |
577 (case apply false tr st of |
577 (case apply (! debug) tr st of |
578 SOME (st', NONE) => |
578 SOME (st', NONE) => |
579 excur trs (st', transform_error (fn () => pr st st' res) () handle exn => |
579 excur trs (st', transform_error (fn () => pr st st' res) () handle exn => |
580 raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr)) |
580 raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr)) |
581 | SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info |
581 | SOME (st', SOME exn_info) => raise EXCURSION_FAIL exn_info |
582 | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); |
582 | NONE => raise EXCURSION_FAIL (TERMINATE, at_command tr)); |