# HG changeset patch # User wenzelm # Date 1375390072 -7200 # Node ID 1a03ffc00a4aa794fa33089c9dc3f15e6144f791 # Parent 0906c00bb21d391ed7d0f64e9b0f5002193246d1 exception trace for Poly/ML 5.5.1, using regular Isabelle output; diff -r 0906c00bb21d -r 1a03ffc00a4a src/Pure/ML/exn_trace_polyml-5.5.1.ML --- /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); + diff -r 0906c00bb21d -r 1a03ffc00a4a src/Pure/ROOT --- 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" diff -r 0906c00bb21d -r 1a03ffc00a4a src/Pure/ROOT.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";