src/Pure/Isar/toplevel.ML
changeset 10324 498999fd7c37
parent 9512 c30f6d0f81d2
child 11894 39a3ece43772
equal deleted inserted replaced
10323:b52d32a11476 10324:498999fd7c37
   428 fun excur [] x = x
   428 fun excur [] x = x
   429   | excur ((tr, f) :: trs) (st, res) =
   429   | excur ((tr, f) :: trs) (st, res) =
   430       (case apply false tr st of
   430       (case apply false tr st of
   431         Some (st', None) =>
   431         Some (st', None) =>
   432           excur trs (st', transform_error (fn () => f st' res) () handle exn =>
   432           excur trs (st', transform_error (fn () => f st' res) () handle exn =>
   433             raise EXCURSION_FAIL (exn, "Presentation failed.\n" ^ at_command tr))
   433             raise EXCURSION_FAIL (exn, "Presentation failed\n" ^ at_command tr))
   434       | Some (st', Some exn_info) => raise EXCURSION_FAIL exn_info
   434       | Some (st', Some exn_info) => raise EXCURSION_FAIL exn_info
   435       | None => raise EXCURSION_FAIL (TERMINATE, at_command tr));
   435       | None => raise EXCURSION_FAIL (TERMINATE, at_command tr));
   436 
   436 
   437 in
   437 in
   438 
   438