exception trace for Poly/ML 5.5.1, using regular Isabelle output;
authorwenzelm
Thu Aug 01 22:47:52 2013 +0200 (2013-08-01)
changeset 528361a03ffc00a4a
parent 52835 0906c00bb21d
child 52837 fe1f6a1707f7
exception trace for Poly/ML 5.5.1, using regular Isabelle output;
src/Pure/ML/exn_trace_polyml-5.5.1.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Thu Aug 01 22:47:52 2013 +0200
     1.3 @@ -0,0 +1,14 @@
     1.4 +(*  Title:      Pure/ML/exn_trace_polyml-5.5.1.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Exception trace for Poly/ML 5.5.1, using regular Isabelle output.
     1.8 +*)
     1.9 +
    1.10 +fun exception_trace e =
    1.11 +  PolyML.Exception.traceException
    1.12 +    (e, fn (trace, exn) =>
    1.13 +      let
    1.14 +        val title = "Exception trace - " ^ ML_Compiler.exn_message exn;
    1.15 +        val _ = tracing (cat_lines (title :: trace));
    1.16 +      in reraise exn end);
    1.17 +
     2.1 --- a/src/Pure/ROOT	Thu Aug 01 22:20:07 2013 +0200
     2.2 +++ b/src/Pure/ROOT	Thu Aug 01 22:47:52 2013 +0200
     2.3 @@ -138,6 +138,7 @@
     2.4      "Isar/typedecl.ML"
     2.5      "ML/exn_properties_dummy.ML"
     2.6      "ML/exn_properties_polyml.ML"
     2.7 +    "ML/exn_trace_polyml-5.5.1.ML"
     2.8      "ML/install_pp_polyml.ML"
     2.9      "ML/ml_antiquote.ML"
    2.10      "ML/ml_compiler.ML"
     3.1 --- a/src/Pure/ROOT.ML	Thu Aug 01 22:20:07 2013 +0200
     3.2 +++ b/src/Pure/ROOT.ML	Thu Aug 01 22:47:52 2013 +0200
     3.3 @@ -183,6 +183,7 @@
     3.4  use "Isar/runtime.ML";
     3.5  use "ML/ml_compiler.ML";
     3.6  if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
     3.7 +if ML_System.name = "polyml-5.5.1" then use "ML/exn_trace_polyml-5.5.1.ML" else ();
     3.8  
     3.9  use "skip_proof.ML";
    3.10  use "goal.ML";