use_text: explicitly print exception, which is no longer done by the new PolyML.compiler setup;
--- 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;