src/Pure/PIDE/document.ML
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;