exception trace for Poly/ML 5.5.1, using regular Isabelle output;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Thu Aug 01 22:47:52 2013 +0200
@@ -0,0 +1,14 @@
+(*  Title:      Pure/ML/exn_trace_polyml-5.5.1.ML
+    Author:     Makarius
+
+Exception trace for Poly/ML 5.5.1, using regular Isabelle output.
+*)
+
+fun exception_trace e =
+  PolyML.Exception.traceException
+    (e, fn (trace, exn) =>
+      let
+        val title = "Exception trace - " ^ ML_Compiler.exn_message exn;
+        val _ = tracing (cat_lines (title :: trace));
+      in reraise exn end);
+

--- a/src/Pure/ROOT	Thu Aug 01 22:20:07 2013 +0200
+++ b/src/Pure/ROOT	Thu Aug 01 22:47:52 2013 +0200
@@ -138,6 +138,7 @@
     "Isar/typedecl.ML"
     "ML/exn_properties_dummy.ML"
     "ML/exn_properties_polyml.ML"
+    "ML/exn_trace_polyml-5.5.1.ML"
     "ML/install_pp_polyml.ML"
     "ML/ml_antiquote.ML"
     "ML/ml_compiler.ML"

--- a/src/Pure/ROOT.ML	Thu Aug 01 22:20:07 2013 +0200
+++ b/src/Pure/ROOT.ML	Thu Aug 01 22:47:52 2013 +0200
@@ -183,6 +183,7 @@
 use "Isar/runtime.ML";
 use "ML/ml_compiler.ML";
 if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
+if ML_System.name = "polyml-5.5.1" then use "ML/exn_trace_polyml-5.5.1.ML" else ();
 
 use "skip_proof.ML";
 use "goal.ML";