# HG changeset patch
# User wenzelm
# Date 1207853658 -7200
# Node ID e0cc4169626e2b9f55297ce24a3a3c6160ce2453
# Parent  7702650329997e8635501efddec44e07f8024afe
use_text: explicitly print exception, which is no longer done by the new PolyML.compiler setup;

diff -r 770265032999 -r e0cc4169626e 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;