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