tuned bootstrap;
authorwenzelm
Thu Jan 29 16:16:01 2015 +0100 (2015-01-29)
changeset 5947031d810570879
parent 59469 fb393ecde29d
child 59471 ca459352d8c5
tuned bootstrap;
src/Pure/ML-Systems/exn_trace_polyml-5.5.1.ML
src/Pure/ML-Systems/polyml.ML
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-Systems/exn_trace_polyml-5.5.1.ML	Thu Jan 29 16:16:01 2015 +0100
     1.3 @@ -0,0 +1,16 @@
     1.4 +(*  Title:      Pure/ML-Systems/exn_trace_polyml-5.5.1.ML
     1.5 +    Author:     Makarius
     1.6 +
     1.7 +Exception trace for Poly/ML 5.5.1 via ML output.
     1.8 +*)
     1.9 +
    1.10 +fun print_exception_trace exn_message output e =
    1.11 +  PolyML.Exception.traceException
    1.12 +    (e, fn (trace, exn) =>
    1.13 +      let
    1.14 +        val title = "Exception trace - " ^ exn_message exn;
    1.15 +        val _ = output (String.concatWith "\n" (title :: trace));
    1.16 +      in reraise exn end);
    1.17 +
    1.18 +PolyML.Compiler.reportExhaustiveHandlers := true;
    1.19 +
     2.1 --- a/src/Pure/ML-Systems/polyml.ML	Thu Jan 29 15:27:29 2015 +0100
     2.2 +++ b/src/Pure/ML-Systems/polyml.ML	Thu Jan 29 16:16:01 2015 +0100
     2.3 @@ -53,6 +53,14 @@
     2.4  
     2.5  use "General/exn.ML";
     2.6  
     2.7 +fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
     2.8 +
     2.9 +if ML_System.name = "polyml-5.5.1"
    2.10 +  orelse ML_System.name = "polyml-5.5.2"
    2.11 +  orelse ML_System.name = "polyml-5.5.3"
    2.12 +then use "ML-Systems/exn_trace_polyml-5.5.1.ML"
    2.13 +else ();
    2.14 +
    2.15  
    2.16  (* multithreading *)
    2.17  
    2.18 @@ -98,7 +106,6 @@
    2.19  
    2.20  (* ML runtime system *)
    2.21  
    2.22 -fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
    2.23  val timing = PolyML.timing;
    2.24  val profiling = PolyML.profiling;
    2.25  
     3.1 --- a/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Thu Jan 29 15:27:29 2015 +0100
     3.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.3 @@ -1,16 +0,0 @@
     3.4 -(*  Title:      Pure/ML/exn_trace_polyml-5.5.1.ML
     3.5 -    Author:     Makarius
     3.6 -
     3.7 -Exception trace for Poly/ML 5.5.1, using regular Isabelle output.
     3.8 -*)
     3.9 -
    3.10 -fun print_exception_trace exn_message output e =
    3.11 -  PolyML.Exception.traceException
    3.12 -    (e, fn (trace, exn) =>
    3.13 -      let
    3.14 -        val title = "Exception trace - " ^ exn_message exn;
    3.15 -        val _ = output (cat_lines (title :: trace));
    3.16 -      in reraise exn end);
    3.17 -
    3.18 -PolyML.Compiler.reportExhaustiveHandlers := true;
    3.19 -
     4.1 --- a/src/Pure/ROOT	Thu Jan 29 15:27:29 2015 +0100
     4.2 +++ b/src/Pure/ROOT	Thu Jan 29 16:16:01 2015 +0100
     4.3 @@ -5,6 +5,7 @@
     4.4    files
     4.5      "General/exn.ML"
     4.6      "ML-Systems/compiler_polyml.ML"
     4.7 +    "ML-Systems/exn_trace_polyml-5.5.1.ML"
     4.8      "ML-Systems/ml_name_space.ML"
     4.9      "ML-Systems/ml_positions.ML"
    4.10      "ML-Systems/ml_pretty.ML"
    4.11 @@ -31,6 +32,7 @@
    4.12    files
    4.13      "General/exn.ML"
    4.14      "ML-Systems/compiler_polyml.ML"
    4.15 +    "ML-Systems/exn_trace_polyml-5.5.1.ML"
    4.16      "ML-Systems/ml_name_space.ML"
    4.17      "ML-Systems/ml_positions.ML"
    4.18      "ML-Systems/ml_pretty.ML"
    4.19 @@ -149,7 +151,6 @@
    4.20      "ML/exn_output_polyml.ML"
    4.21      "ML/exn_properties_dummy.ML"
    4.22      "ML/exn_properties_polyml.ML"
    4.23 -    "ML/exn_trace_polyml-5.5.1.ML"
    4.24      "ML/install_pp_polyml.ML"
    4.25      "ML/ml_antiquotation.ML"
    4.26      "ML/ml_compiler.ML"
     5.1 --- a/src/Pure/ROOT.ML	Thu Jan 29 15:27:29 2015 +0100
     5.2 +++ b/src/Pure/ROOT.ML	Thu Jan 29 16:16:01 2015 +0100
     5.3 @@ -94,12 +94,6 @@
     5.4  then use "ML/exn_properties_polyml.ML"
     5.5  else use "ML/exn_properties_dummy.ML";
     5.6  
     5.7 -if ML_System.name = "polyml-5.5.1"
     5.8 -  orelse ML_System.name = "polyml-5.5.2"
     5.9 -  orelse ML_System.name = "polyml-5.5.3"
    5.10 -then use "ML/exn_trace_polyml-5.5.1.ML"
    5.11 -else ();
    5.12 -
    5.13  if ML_System.name = "polyml-5.5.0"
    5.14    orelse ML_System.name = "polyml-5.5.1"
    5.15    orelse ML_System.name = "polyml-5.5.2"