1.1 --- a/src/Pure/General/basics.ML	Sat Jun 06 21:46:36 2009 +0200
     1.2 +++ b/src/Pure/General/basics.ML	Sat Jun 06 21:47:02 2009 +0200
     1.3 @@ -94,7 +94,7 @@
     1.4  (* partiality *)
     1.5  
     1.6  fun try f x = SOME (f x)
     1.7 -  handle Exn.Interrupt => raise Exn.Interrupt | _ => NONE;
     1.8 +  handle (exn as Exn.Interrupt) => reraise exn | _ => NONE;
     1.9  
    1.10  fun can f x = is_some (try f x);
    1.11  

     2.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Sat Jun 06 21:46:36 2009 +0200
     2.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.0.ML	Sat Jun 06 21:47:02 2009 +0200
     2.3 @@ -21,7 +21,7 @@
     2.4          [] => ()
     2.5        | _ => (PolyML.compilerEx (get, put, fn () => ! current_line, name) (); exec ()));
     2.6    in
     2.7 -    exec () handle exn => (error (output ()); raise exn);
     2.8 +    exec () handle exn => (error (output ()); reraise exn);
     2.9      if verbose then print (output ()) else ()
    2.10    end;
    2.11  

     3.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Sat Jun 06 21:46:36 2009 +0200
     3.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.2.ML	Sat Jun 06 21:47:02 2009 +0200
     3.3 @@ -38,7 +38,7 @@
     3.4          PolyML.compiler (get, parameters) ())
     3.5        handle exn =>
     3.6         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
     3.7 -        error (output ()); raise exn);
     3.8 +        error (output ()); reraise exn);
     3.9    in if verbose then print (output ()) else () end;
    3.10  
    3.11  fun use_file context verbose name =

     4.1 --- a/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Sat Jun 06 21:46:36 2009 +0200
     4.2 +++ b/src/Pure/ML-Systems/compiler_polyml-5.3.ML	Sat Jun 06 21:47:02 2009 +0200
     4.3 @@ -42,7 +42,7 @@
     4.4          PolyML.compiler (get, parameters) ())
     4.5        handle exn =>
     4.6         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
     4.7 -        error (output ()); raise exn);
     4.8 +        error (output ()); reraise exn);
     4.9    in if verbose then print (output ()) else () end;
    4.10  
    4.11  fun use_file context verbose name =

     5.1 --- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sat Jun 06 21:46:36 2009 +0200
     5.2 +++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Sat Jun 06 21:47:02 2009 +0200
     5.3 @@ -173,7 +173,7 @@
     5.4          PolyML.compiler (get, parameters) ())
     5.5        handle exn =>
     5.6         (put ("Exception- " ^ General.exnMessage exn ^ " raised");
     5.7 -        err (output ()); raise exn);
     5.8 +        err (output ()); reraise exn);
     5.9    in if verbose then print (output ()) else () end;
    5.10  
    5.11  end;