improved printing of exception trace in Poly/ML 5.5.1;

--- a/NEWS	Wed Sep 18 11:36:12 2013 +0200
+++ b/NEWS	Wed Sep 18 13:18:51 2013 +0200
@@ -402,6 +402,11 @@
 
 *** ML ***
 
+* Improved printing of exception trace in Poly/ML 5.5.1, with regular
+tracing output in the command transaction context instead of physical
+stdout.  See also Toplevel.debug, Toplevel.debugging and
+ML_Compiler.exn_trace.
+
 * Spec_Check is a Quickcheck tool for Isabelle/ML.  The ML function
 "check_property" allows to check specifications of the form "ALL x y
 z. prop x y z".  See also ~~/src/Tools/Spec_Check/ with its

--- a/src/Doc/IsarImplementation/Integration.thy	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Doc/IsarImplementation/Integration.thy	Wed Sep 18 13:18:51 2013 +0200
@@ -79,10 +79,8 @@
   \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
   state if available, otherwise raises @{ML Toplevel.UNDEF}.
 
-  \item @{ML "Toplevel.debug := true"} enables low-level exception
-  trace of the ML runtime system.  Note that the result might appear
-  on some raw output window only, outside the formal context of the
-  source text.
+  \item @{ML "Toplevel.debug := true"} enables exception trace of the
+  ML runtime system.
 
   \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
   information for each Isar command being executed.

--- a/src/Doc/IsarImplementation/ML.thy	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Doc/IsarImplementation/ML.thy	Wed Sep 18 13:18:51 2013 +0200
@@ -1163,7 +1163,7 @@
   @{index_ML Fail: "string -> exn"} \\
   @{index_ML Exn.is_interrupt: "exn -> bool"} \\
   @{index_ML reraise: "exn -> 'a"} \\
-  @{index_ML exception_trace: "(unit -> 'a) -> 'a"} \\
+  @{index_ML ML_Compiler.exn_trace: "(unit -> 'a) -> 'a"} \\
   \end{mldecls}
 
   \begin{description}
@@ -1191,14 +1191,13 @@
   while preserving its implicit position information (if possible,
   depending on the ML platform).
 
-  \item @{ML exception_trace}~@{ML_text "(fn () =>"}~@{text
+  \item @{ML ML_Compiler.exn_trace}~@{ML_text "(fn () =>"}~@{text
   "e"}@{ML_text ")"} evaluates expression @{text "e"} while printing
   a full trace of its stack of nested exceptions (if possible,
-  depending on the ML platform).\footnote{In versions of Poly/ML the
-  trace will appear on raw stdout of the Isabelle process.}
+  depending on the ML platform).}
 
-  Inserting @{ML exception_trace} into ML code temporarily is useful
-  for debugging, but not suitable for production code.
+  Inserting @{ML ML_Compiler.exn_trace} into ML code temporarily is
+  useful for debugging, but not suitable for production code.
 
   \end{description}
 *}

--- a/src/Pure/Concurrent/simple_thread.ML	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Pure/Concurrent/simple_thread.ML	Wed Sep 18 13:18:51 2013 +0200
@@ -24,7 +24,7 @@
 
 fun fork interrupts body =
   Thread.fork (fn () =>
-    exception_trace (fn () =>
+    print_exception_trace General.exnMessage (fn () =>
       body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
     attributes interrupts);
 

--- a/src/Pure/Isar/runtime.ML	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Pure/Isar/runtime.ML	Wed Sep 18 13:18:51 2013 +0200
@@ -17,8 +17,8 @@
   val exn_messages_ids: exn_info -> exn -> error list
   val exn_messages: exn_info -> exn -> (serial * string) list
   val exn_message: exn_info -> exn -> string
-  val debugging: ('a -> 'b) -> 'a -> 'b
-  val controlled_execution: ('a -> 'b) -> 'a -> 'b
+  val debugging: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
+  val controlled_execution: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
   val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
 end;
 
@@ -137,13 +137,13 @@
 
 (** controlled execution **)
 
-fun debugging f x =
+fun debugging exn_message f x =
   if ! debug
-  then exception_trace (fn () => f x)
+  then print_exception_trace exn_message (fn () => f x)
   else f x;
 
-fun controlled_execution f x =
-  (f |> debugging |> Future.interruptible_task) x;
+fun controlled_execution exn_message f x =
+  (f |> debugging exn_message |> Future.interruptible_task) x;
 
 fun toplevel_error output_exn f x = f x
   handle exn =>

--- a/src/Pure/Isar/toplevel.ML	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Pure/Isar/toplevel.ML	Wed Sep 18 13:18:51 2013 +0200
@@ -26,10 +26,12 @@
   val print_state: bool -> state -> unit
   val pretty_abstract: state -> Pretty.T
   val quiet: bool Unsynchronized.ref
-  val debug: bool Unsynchronized.ref
   val interact: bool Unsynchronized.ref
   val timing: bool Unsynchronized.ref
   val profiling: int Unsynchronized.ref
+  val debug: bool Unsynchronized.ref
+  val debugging: ('a -> 'b) -> 'a -> 'b
+  val controlled_execution: ('a -> 'b) -> 'a -> 'b
   val program: (unit -> 'a) -> 'a
   val thread: bool -> (unit -> unit) -> Thread.thread
   type transition
@@ -226,20 +228,26 @@
 (** toplevel transitions **)
 
 val quiet = Unsynchronized.ref false;  (*Proof General legacy*)
-val debug = Runtime.debug;
 val interact = Unsynchronized.ref false;  (*Proof General legacy*)
 val timing = Unsynchronized.ref false;  (*Proof General legacy*)
 val profiling = Unsynchronized.ref 0;
 
+
+(* controlled execution *)
+
+val debug = Runtime.debug;
+fun debugging f = Runtime.debugging ML_Compiler.exn_message f;
+fun controlled_execution f = Runtime.controlled_execution ML_Compiler.exn_message f;
+
 fun program body =
  (body
-  |> Runtime.controlled_execution
+  |> controlled_execution
   |> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) ();
 
 fun thread interrupts body =
   Thread.fork
     (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
-        |> Runtime.debugging
+        |> debugging
         |> Runtime.toplevel_error
           (fn exn =>
             Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
@@ -268,7 +276,7 @@
 
     val (result, err) =
       cont_node
-      |> Runtime.controlled_execution f
+      |> controlled_execution f
       |> state_error NONE
       handle exn => state_error (SOME exn) cont_node;
   in
@@ -297,11 +305,11 @@
 local
 
 fun apply_tr _ (Init f) (State (NONE, _)) =
-      State (SOME (Theory (Context.Theory (Runtime.controlled_execution f ()), NONE)), NONE)
+      State (SOME (Theory (Context.Theory (controlled_execution f ()), NONE)), NONE)
   | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
       exit_transaction state
   | apply_tr int (Keep f) state =
-      Runtime.controlled_execution (fn x => tap (f int) x) state
+      controlled_execution (fn x => tap (f int) x) state
   | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
       apply_transaction (fn x => f int x) g state
   | apply_tr _ _ _ = raise UNDEF;

--- a/src/Pure/ML-Systems/polyml.ML	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Pure/ML-Systems/polyml.ML	Wed Sep 18 13:18:51 2013 +0200
@@ -75,7 +75,7 @@
 
 (* ML runtime system *)
 
-val exception_trace = PolyML.exception_trace;
+fun print_exception_trace (_: exn -> string) = PolyML.exception_trace;
 val timing = PolyML.timing;
 val profiling = PolyML.profiling;
 

--- a/src/Pure/ML-Systems/smlnj.ML	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Pure/ML-Systems/smlnj.ML	Wed Sep 18 13:18:51 2013 +0200
@@ -73,7 +73,7 @@
 fun profile (n: int) f x = f x;
 
 (*dummy implementation*)
-fun exception_trace f = f ();
+fun print_exception_trace (_: exn -> string) f = f ();
 
 
 (* ML command execution *)

--- a/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Wed Sep 18 13:18:51 2013 +0200
@@ -4,11 +4,11 @@
 Exception trace for Poly/ML 5.5.1, using regular Isabelle output.
 *)
 
-fun exception_trace e =
+fun print_exception_trace exn_message e =
   PolyML.Exception.traceException
     (e, fn (trace, exn) =>
       let
-        val title = "Exception trace - " ^ ML_Compiler.exn_message exn;
+        val title = "Exception trace - " ^ exn_message exn;
         val _ = tracing (cat_lines (title :: trace));
       in reraise exn end);
 

--- a/src/Pure/ML/ml_compiler.ML	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Pure/ML/ml_compiler.ML	Wed Sep 18 13:18:51 2013 +0200
@@ -9,6 +9,7 @@
   val exn_messages_ids: exn -> Runtime.error list
   val exn_messages: exn -> (serial * string) list
   val exn_message: exn -> string
+  val exn_trace: (unit -> 'a) -> 'a
   val eval: bool -> Position.T -> ML_Lex.token list -> unit
 end
 
@@ -22,6 +23,7 @@
 val exn_messages_ids = Runtime.exn_messages_ids exn_info;
 val exn_messages = Runtime.exn_messages exn_info;
 val exn_message = Runtime.exn_message exn_info;
+fun exn_trace e = print_exception_trace exn_message e;
 
 fun eval verbose pos toks =
   let

--- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Sep 18 13:18:51 2013 +0200
@@ -36,6 +36,7 @@
 val exn_messages_ids = Runtime.exn_messages_ids exn_info;
 val exn_messages = Runtime.exn_messages exn_info;
 val exn_message = Runtime.exn_message exn_info;
+fun exn_trace e = print_exception_trace exn_message e;
 
 
 (* parse trees *)
@@ -165,7 +166,7 @@
       | SOME code =>
           apply_result
             ((code
-              |> Runtime.debugging
+              |> Runtime.debugging exn_message
               |> Runtime.toplevel_error (err o exn_message)) ())));
 
 

--- a/src/Pure/PIDE/command.ML	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Pure/PIDE/command.ML	Wed Sep 18 13:18:51 2013 +0200
@@ -212,7 +212,7 @@
   Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
 
 fun print_error tr e =
-  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e ()
+  (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution) e ()
     handle exn =>
       if Exn.is_interrupt exn then reraise exn
       else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
@@ -256,7 +256,7 @@
       let
         val params = {command_name = command_name, args = args};
       in
-        (case Exn.capture (Runtime.controlled_execution get_pr) params of
+        (case Exn.capture (Toplevel.controlled_execution get_pr) params of
           Exn.Res NONE => NONE
         | Exn.Res (SOME pr) => SOME (make_print name args pr)
         | Exn.Exn exn => SOME (bad_print name args exn))

--- a/src/Pure/ROOT.ML	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Pure/ROOT.ML	Wed Sep 18 13:18:51 2013 +0200
@@ -75,6 +75,10 @@
 then use "ML/exn_properties_polyml.ML"
 else use "ML/exn_properties_dummy.ML";
 
+if ML_System.name = "polyml-5.5.1"
+then use "ML/exn_trace_polyml-5.5.1.ML"
+else ();
+
 if ML_System.name = "polyml-5.5.0"
 then use "ML/ml_statistics_polyml-5.5.0.ML"
 else use "ML/ml_statistics_dummy.ML";
@@ -184,7 +188,6 @@
 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 ();
 
 (*global execution*)
 use "PIDE/document_id.ML";

--- a/src/Pure/System/isabelle_process.ML	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Pure/System/isabelle_process.ML	Wed Sep 18 13:18:51 2013 +0200
@@ -48,7 +48,7 @@
   (case Symtab.lookup (Synchronized.value commands) name of
     NONE => error ("Undefined Isabelle protocol command " ^ quote name)
   | SOME cmd =>
-      (Runtime.debugging cmd args handle exn =>
+      (Toplevel.debugging cmd args handle exn =>
         error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
           ML_Compiler.exn_message exn)));
 

--- a/src/Tools/WWW_Find/scgi_server.ML	Wed Sep 18 11:36:12 2013 +0200
+++ b/src/Tools/WWW_Find/scgi_server.ML	Wed Sep 18 13:18:51 2013 +0200
@@ -53,7 +53,7 @@
              ConditionVar.wait (thread_wait, thread_wait_mutex));
        add_thread
          (Thread.fork   (* FIXME avoid low-level Poly/ML thread primitives *)
-            (fn () => exception_trace threadf,
+            (fn () => ML_Compiler.exn_trace threadf,
              [Thread.EnableBroadcastInterrupt true,
               Thread.InterruptState
               Thread.InterruptAsynchOnce])))