# HG changeset patch
# User wenzelm
# Date 1422544561 -3600
# Node ID 31d810570879c18a9f88aefe43c9a06214354cc4
# Parent  fb393ecde29d4ce3adcdca053ca3b2a915555937
tuned bootstrap;

diff -r fb393ecde29d -r 31d810570879 src/Pure/ML-Systems/exn_trace_polyml-5.5.1.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/exn_trace_polyml-5.5.1.ML	Thu Jan 29 16:16:01 2015 +0100
@@ -0,0 +1,16 @@
+(*  Title:      Pure/ML-Systems/exn_trace_polyml-5.5.1.ML
+    Author:     Makarius
+
+Exception trace for Poly/ML 5.5.1 via ML output.
+*)
+
+fun print_exception_trace exn_message output e =
+  PolyML.Exception.traceException
+    (e, fn (trace, exn) =>
+      let
+        val title = "Exception trace - " ^ exn_message exn;
+        val _ = output (String.concatWith "\n" (title :: trace));
+      in reraise exn end);
+
+PolyML.Compiler.reportExhaustiveHandlers := true;
+
diff -r fb393ecde29d -r 31d810570879 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Jan 29 15:27:29 2015 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Jan 29 16:16:01 2015 +0100
@@ -53,6 +53,14 @@
 
 use "General/exn.ML";
 
+fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
+
+if ML_System.name = "polyml-5.5.1"
+  orelse ML_System.name = "polyml-5.5.2"
+  orelse ML_System.name = "polyml-5.5.3"
+then use "ML-Systems/exn_trace_polyml-5.5.1.ML"
+else ();
+
 
 (* multithreading *)
 
@@ -98,7 +106,6 @@
 
 (* ML runtime system *)
 
-fun print_exception_trace (_: exn -> string) (_: string -> unit) = PolyML.exception_trace;
 val timing = PolyML.timing;
 val profiling = PolyML.profiling;
 
diff -r fb393ecde29d -r 31d810570879 src/Pure/ML/exn_trace_polyml-5.5.1.ML
--- a/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Thu Jan 29 15:27:29 2015 +0100
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,16 +0,0 @@
-(*  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 print_exception_trace exn_message output e =
-  PolyML.Exception.traceException
-    (e, fn (trace, exn) =>
-      let
-        val title = "Exception trace - " ^ exn_message exn;
-        val _ = output (cat_lines (title :: trace));
-      in reraise exn end);
-
-PolyML.Compiler.reportExhaustiveHandlers := true;
-
diff -r fb393ecde29d -r 31d810570879 src/Pure/ROOT
--- a/src/Pure/ROOT	Thu Jan 29 15:27:29 2015 +0100
+++ b/src/Pure/ROOT	Thu Jan 29 16:16:01 2015 +0100
@@ -5,6 +5,7 @@
   files
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
+    "ML-Systems/exn_trace_polyml-5.5.1.ML"
     "ML-Systems/ml_name_space.ML"
     "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
@@ -31,6 +32,7 @@
   files
     "General/exn.ML"
     "ML-Systems/compiler_polyml.ML"
+    "ML-Systems/exn_trace_polyml-5.5.1.ML"
     "ML-Systems/ml_name_space.ML"
     "ML-Systems/ml_positions.ML"
     "ML-Systems/ml_pretty.ML"
@@ -149,7 +151,6 @@
     "ML/exn_output_polyml.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_antiquotation.ML"
     "ML/ml_compiler.ML"
diff -r fb393ecde29d -r 31d810570879 src/Pure/ROOT.ML
--- a/src/Pure/ROOT.ML	Thu Jan 29 15:27:29 2015 +0100
+++ b/src/Pure/ROOT.ML	Thu Jan 29 16:16:01 2015 +0100
@@ -94,12 +94,6 @@
 then use "ML/exn_properties_polyml.ML"
 else use "ML/exn_properties_dummy.ML";
 
-if ML_System.name = "polyml-5.5.1"
-  orelse ML_System.name = "polyml-5.5.2"
-  orelse ML_System.name = "polyml-5.5.3"
-then use "ML/exn_trace_polyml-5.5.1.ML"
-else ();
-
 if ML_System.name = "polyml-5.5.0"
   orelse ML_System.name = "polyml-5.5.1"
   orelse ML_System.name = "polyml-5.5.2"