changeset 39232 | 69c6d3e87660 |
parent 38888 | 8248cda328de |
child 39238 | 7189a138dd6c |
--- a/src/Pure/PIDE/document.ML Thu Sep 09 11:05:52 2010 +0200 +++ b/src/Pure/PIDE/document.ML Thu Sep 09 17:20:27 2010 +0200 @@ -225,7 +225,7 @@ SOME (st', NONE) => ([], SOME st') | SOME (_, SOME exn_info) => (case ML_Compiler.exn_messages (Runtime.EXCURSION_FAIL exn_info) of - [] => raise Exn.Interrupt + [] => Exn.interrupt () | errs => (errs, NONE)) | NONE => ([ML_Compiler.exn_message Runtime.TERMINATE], NONE)); val _ = List.app (Toplevel.error_msg tr) errs;