equal
deleted
inserted
replaced
266 SOME (st', NONE) => ([], SOME st') |
266 SOME (st', NONE) => ([], SOME st') |
267 | SOME (_, SOME exn_info) => |
267 | SOME (_, SOME exn_info) => |
268 (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of |
268 (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of |
269 [] => Exn.interrupt () |
269 [] => Exn.interrupt () |
270 | errs => (errs, NONE)) |
270 | errs => (errs, NONE)) |
271 | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE)); |
271 | NONE => ([(serial (), ML_Compiler.exn_message Runtime.TERMINATE)], NONE)); |
272 |
272 |
273 in |
273 in |
274 |
274 |
275 fun run_command tr st = |
275 fun run_command tr st = |
276 let |
276 let |