src/Pure/ML-Systems/polyml.ML

--- a/src/Pure/ML-Systems/polyml.ML	Thu Apr 10 20:54:17 2008 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Apr 10 20:54:18 2008 +0200
@@ -31,7 +31,9 @@
         PolyML.compiler
           {getChar = get, putString = put, lineNumber = fn () => ! current_line, fileName = name,
             nameSpace = PolyML.globalNameSpace} ())
-      handle exn => (err (output ()); raise exn);
+      handle exn =>
+       (put ("Exception- " ^ General.exnMessage exn ^ " raised");
+        err (output ()); raise exn);
   in
     if verbose then print (output ()) else ()
   end;