improved printing of exception trace in Poly/ML 5.5.1;
authorwenzelm
Wed Sep 18 13:18:51 2013 +0200 (2013-09-18)
changeset 5370984522727f9d3
parent 53708 92aa282841f8
child 53710 5ec27e55ddc2
improved printing of exception trace in Poly/ML 5.5.1;
NEWS
src/Doc/IsarImplementation/Integration.thy
src/Doc/IsarImplementation/ML.thy
src/Pure/Concurrent/simple_thread.ML
src/Pure/Isar/runtime.ML
src/Pure/Isar/toplevel.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/ML/exn_trace_polyml-5.5.1.ML
src/Pure/ML/ml_compiler.ML
src/Pure/ML/ml_compiler_polyml.ML
src/Pure/PIDE/command.ML
src/Pure/ROOT.ML
src/Pure/System/isabelle_process.ML
src/Tools/WWW_Find/scgi_server.ML
     1.1 --- a/NEWS	Wed Sep 18 11:36:12 2013 +0200
     1.2 +++ b/NEWS	Wed Sep 18 13:18:51 2013 +0200
     1.3 @@ -402,6 +402,11 @@
     1.4  
     1.5  *** ML ***
     1.6  
     1.7 +* Improved printing of exception trace in Poly/ML 5.5.1, with regular
     1.8 +tracing output in the command transaction context instead of physical
     1.9 +stdout.  See also Toplevel.debug, Toplevel.debugging and
    1.10 +ML_Compiler.exn_trace.
    1.11 +
    1.12  * Spec_Check is a Quickcheck tool for Isabelle/ML.  The ML function
    1.13  "check_property" allows to check specifications of the form "ALL x y
    1.14  z. prop x y z".  See also ~~/src/Tools/Spec_Check/ with its
     2.1 --- a/src/Doc/IsarImplementation/Integration.thy	Wed Sep 18 11:36:12 2013 +0200
     2.2 +++ b/src/Doc/IsarImplementation/Integration.thy	Wed Sep 18 13:18:51 2013 +0200
     2.3 @@ -79,10 +79,8 @@
     2.4    \item @{ML Toplevel.proof_of}~@{text "state"} selects the Isar proof
     2.5    state if available, otherwise raises @{ML Toplevel.UNDEF}.
     2.6  
     2.7 -  \item @{ML "Toplevel.debug := true"} enables low-level exception
     2.8 -  trace of the ML runtime system.  Note that the result might appear
     2.9 -  on some raw output window only, outside the formal context of the
    2.10 -  source text.
    2.11 +  \item @{ML "Toplevel.debug := true"} enables exception trace of the
    2.12 +  ML runtime system.
    2.13  
    2.14    \item @{ML "Toplevel.timing := true"} makes the toplevel print timing
    2.15    information for each Isar command being executed.
     3.1 --- a/src/Doc/IsarImplementation/ML.thy	Wed Sep 18 11:36:12 2013 +0200
     3.2 +++ b/src/Doc/IsarImplementation/ML.thy	Wed Sep 18 13:18:51 2013 +0200
     3.3 @@ -1163,7 +1163,7 @@
     3.4    @{index_ML Fail: "string -> exn"} \\
     3.5    @{index_ML Exn.is_interrupt: "exn -> bool"} \\
     3.6    @{index_ML reraise: "exn -> 'a"} \\
     3.7 -  @{index_ML exception_trace: "(unit -> 'a) -> 'a"} \\
     3.8 +  @{index_ML ML_Compiler.exn_trace: "(unit -> 'a) -> 'a"} \\
     3.9    \end{mldecls}
    3.10  
    3.11    \begin{description}
    3.12 @@ -1191,14 +1191,13 @@
    3.13    while preserving its implicit position information (if possible,
    3.14    depending on the ML platform).
    3.15  
    3.16 -  \item @{ML exception_trace}~@{ML_text "(fn () =>"}~@{text
    3.17 +  \item @{ML ML_Compiler.exn_trace}~@{ML_text "(fn () =>"}~@{text
    3.18    "e"}@{ML_text ")"} evaluates expression @{text "e"} while printing
    3.19    a full trace of its stack of nested exceptions (if possible,
    3.20 -  depending on the ML platform).\footnote{In versions of Poly/ML the
    3.21 -  trace will appear on raw stdout of the Isabelle process.}
    3.22 +  depending on the ML platform).}
    3.23  
    3.24 -  Inserting @{ML exception_trace} into ML code temporarily is useful
    3.25 -  for debugging, but not suitable for production code.
    3.26 +  Inserting @{ML ML_Compiler.exn_trace} into ML code temporarily is
    3.27 +  useful for debugging, but not suitable for production code.
    3.28  
    3.29    \end{description}
    3.30  *}
     4.1 --- a/src/Pure/Concurrent/simple_thread.ML	Wed Sep 18 11:36:12 2013 +0200
     4.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Wed Sep 18 13:18:51 2013 +0200
     4.3 @@ -24,7 +24,7 @@
     4.4  
     4.5  fun fork interrupts body =
     4.6    Thread.fork (fn () =>
     4.7 -    exception_trace (fn () =>
     4.8 +    print_exception_trace General.exnMessage (fn () =>
     4.9        body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
    4.10      attributes interrupts);
    4.11  
     5.1 --- a/src/Pure/Isar/runtime.ML	Wed Sep 18 11:36:12 2013 +0200
     5.2 +++ b/src/Pure/Isar/runtime.ML	Wed Sep 18 13:18:51 2013 +0200
     5.3 @@ -17,8 +17,8 @@
     5.4    val exn_messages_ids: exn_info -> exn -> error list
     5.5    val exn_messages: exn_info -> exn -> (serial * string) list
     5.6    val exn_message: exn_info -> exn -> string
     5.7 -  val debugging: ('a -> 'b) -> 'a -> 'b
     5.8 -  val controlled_execution: ('a -> 'b) -> 'a -> 'b
     5.9 +  val debugging: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
    5.10 +  val controlled_execution: (exn -> string) -> ('a -> 'b) -> 'a -> 'b
    5.11    val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
    5.12  end;
    5.13  
    5.14 @@ -137,13 +137,13 @@
    5.15  
    5.16  (** controlled execution **)
    5.17  
    5.18 -fun debugging f x =
    5.19 +fun debugging exn_message f x =
    5.20    if ! debug
    5.21 -  then exception_trace (fn () => f x)
    5.22 +  then print_exception_trace exn_message (fn () => f x)
    5.23    else f x;
    5.24  
    5.25 -fun controlled_execution f x =
    5.26 -  (f |> debugging |> Future.interruptible_task) x;
    5.27 +fun controlled_execution exn_message f x =
    5.28 +  (f |> debugging exn_message |> Future.interruptible_task) x;
    5.29  
    5.30  fun toplevel_error output_exn f x = f x
    5.31    handle exn =>
     6.1 --- a/src/Pure/Isar/toplevel.ML	Wed Sep 18 11:36:12 2013 +0200
     6.2 +++ b/src/Pure/Isar/toplevel.ML	Wed Sep 18 13:18:51 2013 +0200
     6.3 @@ -26,10 +26,12 @@
     6.4    val print_state: bool -> state -> unit
     6.5    val pretty_abstract: state -> Pretty.T
     6.6    val quiet: bool Unsynchronized.ref
     6.7 -  val debug: bool Unsynchronized.ref
     6.8    val interact: bool Unsynchronized.ref
     6.9    val timing: bool Unsynchronized.ref
    6.10    val profiling: int Unsynchronized.ref
    6.11 +  val debug: bool Unsynchronized.ref
    6.12 +  val debugging: ('a -> 'b) -> 'a -> 'b
    6.13 +  val controlled_execution: ('a -> 'b) -> 'a -> 'b
    6.14    val program: (unit -> 'a) -> 'a
    6.15    val thread: bool -> (unit -> unit) -> Thread.thread
    6.16    type transition
    6.17 @@ -226,20 +228,26 @@
    6.18  (** toplevel transitions **)
    6.19  
    6.20  val quiet = Unsynchronized.ref false;  (*Proof General legacy*)
    6.21 -val debug = Runtime.debug;
    6.22  val interact = Unsynchronized.ref false;  (*Proof General legacy*)
    6.23  val timing = Unsynchronized.ref false;  (*Proof General legacy*)
    6.24  val profiling = Unsynchronized.ref 0;
    6.25  
    6.26 +
    6.27 +(* controlled execution *)
    6.28 +
    6.29 +val debug = Runtime.debug;
    6.30 +fun debugging f = Runtime.debugging ML_Compiler.exn_message f;
    6.31 +fun controlled_execution f = Runtime.controlled_execution ML_Compiler.exn_message f;
    6.32 +
    6.33  fun program body =
    6.34   (body
    6.35 -  |> Runtime.controlled_execution
    6.36 +  |> controlled_execution
    6.37    |> Runtime.toplevel_error (Output.error_msg o ML_Compiler.exn_message)) ();
    6.38  
    6.39  fun thread interrupts body =
    6.40    Thread.fork
    6.41      (((fn () => body () handle exn => if Exn.is_interrupt exn then () else reraise exn)
    6.42 -        |> Runtime.debugging
    6.43 +        |> debugging
    6.44          |> Runtime.toplevel_error
    6.45            (fn exn =>
    6.46              Output.urgent_message ("## INTERNAL ERROR ##\n" ^ ML_Compiler.exn_message exn))),
    6.47 @@ -268,7 +276,7 @@
    6.48  
    6.49      val (result, err) =
    6.50        cont_node
    6.51 -      |> Runtime.controlled_execution f
    6.52 +      |> controlled_execution f
    6.53        |> state_error NONE
    6.54        handle exn => state_error (SOME exn) cont_node;
    6.55    in
    6.56 @@ -297,11 +305,11 @@
    6.57  local
    6.58  
    6.59  fun apply_tr _ (Init f) (State (NONE, _)) =
    6.60 -      State (SOME (Theory (Context.Theory (Runtime.controlled_execution f ()), NONE)), NONE)
    6.61 +      State (SOME (Theory (Context.Theory (controlled_execution f ()), NONE)), NONE)
    6.62    | apply_tr _ Exit (State (SOME (state as Theory (Context.Theory _, _)), _)) =
    6.63        exit_transaction state
    6.64    | apply_tr int (Keep f) state =
    6.65 -      Runtime.controlled_execution (fn x => tap (f int) x) state
    6.66 +      controlled_execution (fn x => tap (f int) x) state
    6.67    | apply_tr int (Transaction (f, g)) (State (SOME state, _)) =
    6.68        apply_transaction (fn x => f int x) g state
    6.69    | apply_tr _ _ _ = raise UNDEF;
     7.1 --- a/src/Pure/ML-Systems/polyml.ML	Wed Sep 18 11:36:12 2013 +0200
     7.2 +++ b/src/Pure/ML-Systems/polyml.ML	Wed Sep 18 13:18:51 2013 +0200
     7.3 @@ -75,7 +75,7 @@
     7.4  
     7.5  (* ML runtime system *)
     7.6  
     7.7 -val exception_trace = PolyML.exception_trace;
     7.8 +fun print_exception_trace (_: exn -> string) = PolyML.exception_trace;
     7.9  val timing = PolyML.timing;
    7.10  val profiling = PolyML.profiling;
    7.11  
     8.1 --- a/src/Pure/ML-Systems/smlnj.ML	Wed Sep 18 11:36:12 2013 +0200
     8.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Wed Sep 18 13:18:51 2013 +0200
     8.3 @@ -73,7 +73,7 @@
     8.4  fun profile (n: int) f x = f x;
     8.5  
     8.6  (*dummy implementation*)
     8.7 -fun exception_trace f = f ();
     8.8 +fun print_exception_trace (_: exn -> string) f = f ();
     8.9  
    8.10  
    8.11  (* ML command execution *)
     9.1 --- a/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Wed Sep 18 11:36:12 2013 +0200
     9.2 +++ b/src/Pure/ML/exn_trace_polyml-5.5.1.ML	Wed Sep 18 13:18:51 2013 +0200
     9.3 @@ -4,11 +4,11 @@
     9.4  Exception trace for Poly/ML 5.5.1, using regular Isabelle output.
     9.5  *)
     9.6  
     9.7 -fun exception_trace e =
     9.8 +fun print_exception_trace exn_message e =
     9.9    PolyML.Exception.traceException
    9.10      (e, fn (trace, exn) =>
    9.11        let
    9.12 -        val title = "Exception trace - " ^ ML_Compiler.exn_message exn;
    9.13 +        val title = "Exception trace - " ^ exn_message exn;
    9.14          val _ = tracing (cat_lines (title :: trace));
    9.15        in reraise exn end);
    9.16  
    10.1 --- a/src/Pure/ML/ml_compiler.ML	Wed Sep 18 11:36:12 2013 +0200
    10.2 +++ b/src/Pure/ML/ml_compiler.ML	Wed Sep 18 13:18:51 2013 +0200
    10.3 @@ -9,6 +9,7 @@
    10.4    val exn_messages_ids: exn -> Runtime.error list
    10.5    val exn_messages: exn -> (serial * string) list
    10.6    val exn_message: exn -> string
    10.7 +  val exn_trace: (unit -> 'a) -> 'a
    10.8    val eval: bool -> Position.T -> ML_Lex.token list -> unit
    10.9  end
   10.10  
   10.11 @@ -22,6 +23,7 @@
   10.12  val exn_messages_ids = Runtime.exn_messages_ids exn_info;
   10.13  val exn_messages = Runtime.exn_messages exn_info;
   10.14  val exn_message = Runtime.exn_message exn_info;
   10.15 +fun exn_trace e = print_exception_trace exn_message e;
   10.16  
   10.17  fun eval verbose pos toks =
   10.18    let
    11.1 --- a/src/Pure/ML/ml_compiler_polyml.ML	Wed Sep 18 11:36:12 2013 +0200
    11.2 +++ b/src/Pure/ML/ml_compiler_polyml.ML	Wed Sep 18 13:18:51 2013 +0200
    11.3 @@ -36,6 +36,7 @@
    11.4  val exn_messages_ids = Runtime.exn_messages_ids exn_info;
    11.5  val exn_messages = Runtime.exn_messages exn_info;
    11.6  val exn_message = Runtime.exn_message exn_info;
    11.7 +fun exn_trace e = print_exception_trace exn_message e;
    11.8  
    11.9  
   11.10  (* parse trees *)
   11.11 @@ -165,7 +166,7 @@
   11.12        | SOME code =>
   11.13            apply_result
   11.14              ((code
   11.15 -              |> Runtime.debugging
   11.16 +              |> Runtime.debugging exn_message
   11.17                |> Runtime.toplevel_error (err o exn_message)) ())));
   11.18  
   11.19  
    12.1 --- a/src/Pure/PIDE/command.ML	Wed Sep 18 11:36:12 2013 +0200
    12.2 +++ b/src/Pure/PIDE/command.ML	Wed Sep 18 13:18:51 2013 +0200
    12.3 @@ -212,7 +212,7 @@
    12.4    Synchronized.var "Command.print_functions" ([]: (string * print_function) list);
    12.5  
    12.6  fun print_error tr e =
    12.7 -  (Toplevel.setmp_thread_position tr o Runtime.controlled_execution) e ()
    12.8 +  (Toplevel.setmp_thread_position tr o Toplevel.controlled_execution) e ()
    12.9      handle exn =>
   12.10        if Exn.is_interrupt exn then reraise exn
   12.11        else List.app (Future.error_msg (Toplevel.pos_of tr)) (ML_Compiler.exn_messages_ids exn);
   12.12 @@ -256,7 +256,7 @@
   12.13        let
   12.14          val params = {command_name = command_name, args = args};
   12.15        in
   12.16 -        (case Exn.capture (Runtime.controlled_execution get_pr) params of
   12.17 +        (case Exn.capture (Toplevel.controlled_execution get_pr) params of
   12.18            Exn.Res NONE => NONE
   12.19          | Exn.Res (SOME pr) => SOME (make_print name args pr)
   12.20          | Exn.Exn exn => SOME (bad_print name args exn))
    13.1 --- a/src/Pure/ROOT.ML	Wed Sep 18 11:36:12 2013 +0200
    13.2 +++ b/src/Pure/ROOT.ML	Wed Sep 18 13:18:51 2013 +0200
    13.3 @@ -75,6 +75,10 @@
    13.4  then use "ML/exn_properties_polyml.ML"
    13.5  else use "ML/exn_properties_dummy.ML";
    13.6  
    13.7 +if ML_System.name = "polyml-5.5.1"
    13.8 +then use "ML/exn_trace_polyml-5.5.1.ML"
    13.9 +else ();
   13.10 +
   13.11  if ML_System.name = "polyml-5.5.0"
   13.12  then use "ML/ml_statistics_polyml-5.5.0.ML"
   13.13  else use "ML/ml_statistics_dummy.ML";
   13.14 @@ -184,7 +188,6 @@
   13.15  use "Isar/runtime.ML";
   13.16  use "ML/ml_compiler.ML";
   13.17  if ML_System.is_polyml then use "ML/ml_compiler_polyml.ML" else ();
   13.18 -if ML_System.name = "polyml-5.5.1" then use "ML/exn_trace_polyml-5.5.1.ML" else ();
   13.19  
   13.20  (*global execution*)
   13.21  use "PIDE/document_id.ML";
    14.1 --- a/src/Pure/System/isabelle_process.ML	Wed Sep 18 11:36:12 2013 +0200
    14.2 +++ b/src/Pure/System/isabelle_process.ML	Wed Sep 18 13:18:51 2013 +0200
    14.3 @@ -48,7 +48,7 @@
    14.4    (case Symtab.lookup (Synchronized.value commands) name of
    14.5      NONE => error ("Undefined Isabelle protocol command " ^ quote name)
    14.6    | SOME cmd =>
    14.7 -      (Runtime.debugging cmd args handle exn =>
    14.8 +      (Toplevel.debugging cmd args handle exn =>
    14.9          error ("Isabelle protocol command failure: " ^ quote name ^ "\n" ^
   14.10            ML_Compiler.exn_message exn)));
   14.11  
    15.1 --- a/src/Tools/WWW_Find/scgi_server.ML	Wed Sep 18 11:36:12 2013 +0200
    15.2 +++ b/src/Tools/WWW_Find/scgi_server.ML	Wed Sep 18 13:18:51 2013 +0200
    15.3 @@ -53,7 +53,7 @@
    15.4               ConditionVar.wait (thread_wait, thread_wait_mutex));
    15.5         add_thread
    15.6           (Thread.fork   (* FIXME avoid low-level Poly/ML thread primitives *)
    15.7 -            (fn () => exception_trace threadf,
    15.8 +            (fn () => ML_Compiler.exn_trace threadf,
    15.9               [Thread.EnableBroadcastInterrupt true,
   15.10                Thread.InterruptState
   15.11                Thread.InterruptAsynchOnce])))