# HG changeset patch
# User wenzelm
# Date 1283982744 -7200
# Node ID 184507f6e8d0dc2d1520b7f9f8c2d0fa0d0033a9
# Parent  6530e87186c95c359fa3a312b85dccc992b580e6
ML_Compiler.eval: discontinued extra "Static Errors" of raw Poly/ML;

diff -r 6530e87186c9 -r 184507f6e8d0 src/Pure/ML/ml_compiler_polyml-5.3.ML
--- a/src/Pure/ML/ml_compiler_polyml-5.3.ML	Wed Sep 08 23:40:48 2010 +0200
+++ b/src/Pure/ML/ml_compiler_polyml-5.3.ML	Wed Sep 08 23:52:24 2010 +0200
@@ -158,12 +158,14 @@
         List.app apply_val values
       end;
 
+    exception Static_Errors of unit;
+
     fun result_fun (phase1, phase2) () =
      ((case phase1 of
         NONE => ()
       | SOME parse_tree => report_parse_tree depth space parse_tree);
       (case phase2 of
-        NONE => error "Static Errors"
+        NONE => raise Static_Errors ()
       | SOME code =>
           apply_result
             ((code
@@ -188,7 +190,8 @@
       handle exn =>
        (output_warnings ();
         output_writeln ();
-        raise_error ("Exception- " ^ General.exnMessage exn ^ " raised"));
+        (case exn of Static_Errors () => raise_error ""
+        | _ => raise_error ("Exception- " ^ General.exnMessage exn ^ " raised")));
   in
     if verbose then (output_warnings (); flush_error (); output_writeln ())
     else ()