src/Pure/ML/ml_compiler_polyml-5.3.ML
changeset 39232 69c6d3e87660
parent 39231 25c345302a17
child 39240 a0c0698e56c0
     1.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Thu Sep 09 11:05:52 2010 +0200
     1.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Thu Sep 09 17:20:27 2010 +0200
     1.3 @@ -186,17 +186,18 @@
     1.4      val _ =
     1.5        (while not (List.null (! input_buffer)) do
     1.6          PolyML.compiler (get, parameters) ())
     1.7 -      handle exn as Exn.Interrupt => reraise exn
     1.8 -        | exn =>
     1.9 -            let
    1.10 -              val exn_msg =
    1.11 -                (case exn of
    1.12 -                  STATIC_ERRORS () => ""
    1.13 -                | Runtime.TOPLEVEL_ERROR => ""
    1.14 -                | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
    1.15 -              val _ = output_warnings ();
    1.16 -              val _ = output_writeln ();
    1.17 -            in raise_error exn_msg end;
    1.18 +      handle exn =>
    1.19 +        if Exn.is_interrupt exn then reraise exn
    1.20 +        else
    1.21 +          let
    1.22 +            val exn_msg =
    1.23 +              (case exn of
    1.24 +                STATIC_ERRORS () => ""
    1.25 +              | Runtime.TOPLEVEL_ERROR => ""
    1.26 +              | _ => "Exception- " ^ General.exnMessage exn ^ " raised");
    1.27 +            val _ = output_warnings ();
    1.28 +            val _ = output_writeln ();
    1.29 +          in raise_error exn_msg end;
    1.30    in
    1.31      if verbose then (output_warnings (); flush_error (); output_writeln ())
    1.32      else ()