--- a/NEWS Wed Mar 02 10:02:12 2016 +0100
+++ b/NEWS Wed Mar 02 19:43:31 2016 +0100
@@ -181,6 +181,15 @@
* Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis.
+*** ML ***
+
+* Option ML_exception_debugger controls detailed exception trace via the
+Poly/ML debugger. Relevant ML modules need to be compiled beforehand
+with ML_file_debug, or with ML_file and option ML_debugger enabled. Note
+debugger information requires consirable time and space: main
+Isabelle/HOL with full debugger support may need ML_system_64.
+
+
*** System ***
* The Isabelle system environment always ensures that the main
--- a/etc/options Wed Mar 02 10:02:12 2016 +0100
+++ b/etc/options Wed Mar 02 19:43:31 2016 +0100
@@ -107,6 +107,9 @@
public option ML_exception_trace : bool = false
-- "ML exception trace for toplevel command execution"
+public option ML_exception_debugger : bool = false
+ -- "ML debugger exception trace for toplevel command execution"
+
public option ML_debugger : bool = false
-- "ML debugger instrumentation for newly compiled code"
--- a/src/Pure/Isar/attrib.ML Wed Mar 02 10:02:12 2016 +0100
+++ b/src/Pure/Isar/attrib.ML Wed Mar 02 19:43:31 2016 +0100
@@ -519,6 +519,7 @@
register_config Name_Space.names_unique_raw #>
register_config ML_Options.source_trace_raw #>
register_config ML_Options.exception_trace_raw #>
+ register_config ML_Options.exception_debugger_raw #>
register_config ML_Options.debugger_raw #>
register_config ML_Options.print_depth_raw #>
register_config Proof_Context.show_abbrevs_raw #>
--- a/src/Pure/Isar/runtime.ML Wed Mar 02 10:02:12 2016 +0100
+++ b/src/Pure/Isar/runtime.ML Wed Mar 02 19:43:31 2016 +0100
@@ -19,6 +19,8 @@
val exn_system_message: exn -> unit
val exn_trace: (unit -> 'a) -> 'a
val exn_trace_system: (unit -> 'a) -> 'a
+ val exn_debugger: (unit -> 'a) -> 'a
+ val exn_debugger_system: (unit -> 'a) -> 'a
val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
@@ -143,13 +145,45 @@
fun exn_trace_system e = print_exception_trace exn_message Output.system_message e;
+(* exception debugger *)
+
+local
+
+fun print_entry (name, loc) =
+ Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of loc));
+
+fun exception_debugger output e =
+ let
+ val (trace, result) = Exn_Debugger.capture_exception_trace e;
+ val _ =
+ (case (trace, result) of
+ (_ :: _, Exn.Exn exn) =>
+ output (cat_lines ("Exception trace - " ^ exn_message exn :: map print_entry trace))
+ | _ => ());
+ in Exn.release result end;
+
+in
+
+fun exn_debugger e = exception_debugger tracing e;
+fun exn_debugger_system e = exception_debugger Output.system_message e;
+
+end;
+
+
(** controlled execution **)
-fun debugging opt_context f x =
+fun debugging1 opt_context f x =
if ML_Options.exception_trace_enabled opt_context
then exn_trace (fn () => f x) else f x;
+fun debugging2 opt_context f x =
+ if ML_Options.exception_debugger_enabled opt_context
+ then exn_debugger (fn () => f x) else f x;
+
+fun debugging opt_context f =
+ f |> debugging1 opt_context |> debugging2 opt_context;
+
fun controlled_execution opt_context f x =
(f |> debugging opt_context |> Future.interruptible_task) x;
@@ -169,4 +203,3 @@
(body |> controlled_execution NONE |> toplevel_error exn_error_message) ();
end;
-
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML/exn_debugger.ML Wed Mar 02 19:43:31 2016 +0100
@@ -0,0 +1,63 @@
+(* Title: Pure/ML/exn_debugger.ML
+ Author: Makarius
+
+Detailed exception trace via ML debugger.
+*)
+
+signature EXN_DEBUGGER =
+sig
+ val capture_exception_trace: (unit -> 'a) -> (string * ML_Debugger.location) list * 'a Exn.result
+end;
+
+structure Exn_Debugger: EXN_DEBUGGER =
+struct
+
+(* thread data *)
+
+local
+ val tag = Universal.tag () : ((string * ML_Debugger.location) * exn) list option Universal.tag;
+in
+
+fun start_trace () = Thread.setLocal (tag, SOME []);
+
+fun update_trace entry exn =
+ (case Thread.getLocal tag of
+ SOME (SOME trace) => Thread.setLocal (tag, SOME ((entry, exn) :: trace))
+ | _ => ());
+
+fun stop_trace () =
+ let
+ val trace = (case Thread.getLocal tag of SOME (SOME trace) => trace | _ => []);
+ val _ = Thread.setLocal (tag, NONE);
+ in trace end;
+
+val _ = ML_Debugger.on_exit_exception (SOME update_trace);
+
+end;
+
+
+(* capture exception trace *)
+
+local
+ fun eq_exn exns =
+ op = (apply2 General.exnName exns) andalso op = (apply2 Exn_Output.position exns);
+in
+
+fun capture_exception_trace e =
+ uninterruptible (fn restore_attributes => fn () =>
+ let
+ val _ = start_trace ();
+ val result = Exn.interruptible_capture (restore_attributes e) ();
+ val trace = stop_trace ();
+ val trace' =
+ (case result of
+ Exn.Res _ => []
+ | Exn.Exn exn =>
+ trace
+ |> map_filter (fn (entry, e) => if eq_exn (exn, e) then SOME entry else NONE)
+ |> rev);
+ in (trace', result) end) ();
+
+end;
+
+end;
--- a/src/Pure/ML/ml_options.ML Wed Mar 02 10:02:12 2016 +0100
+++ b/src/Pure/ML/ml_options.ML Wed Mar 02 19:43:31 2016 +0100
@@ -11,6 +11,9 @@
val exception_trace_raw: Config.raw
val exception_trace: bool Config.T
val exception_trace_enabled: Context.generic option -> bool
+ val exception_debugger_raw: Config.raw
+ val exception_debugger: bool Config.T
+ val exception_debugger_enabled: Context.generic option -> bool
val debugger_raw: Config.raw
val debugger: bool Config.T
val debugger_enabled: Context.generic option -> bool
@@ -40,6 +43,16 @@
| exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
+(* exception debugger *)
+
+val exception_debugger_raw = Config.declare_option ("ML_exception_debugger", @{here});
+val exception_debugger = Config.bool exception_debugger_raw;
+
+fun exception_debugger_enabled NONE =
+ (Options.default_bool (Config.name_of exception_debugger_raw) handle ERROR _ => false)
+ | exception_debugger_enabled (SOME context) = Config.get_generic context exception_debugger;
+
+
(* debugger *)
val debugger_raw = Config.declare_option ("ML_debugger", @{here});
--- a/src/Pure/ROOT Wed Mar 02 10:02:12 2016 +0100
+++ b/src/Pure/ROOT Wed Mar 02 19:43:31 2016 +0100
@@ -157,6 +157,7 @@
"Isar/token.ML"
"Isar/toplevel.ML"
"Isar/typedecl.ML"
+ "ML/exn_debugger.ML"
"ML/exn_output.ML"
"ML/exn_properties.ML"
"ML/install_pp_polyml.ML"
--- a/src/Pure/ROOT.ML Wed Mar 02 10:02:12 2016 +0100
+++ b/src/Pure/ROOT.ML Wed Mar 02 19:43:31 2016 +0100
@@ -190,8 +190,9 @@
use "ML/ml_env.ML";
use "ML/ml_options.ML";
use "ML/exn_output.ML";
+use_no_debug "ML/exn_debugger.ML";
use "ML/ml_options.ML";
-use "Isar/runtime.ML";
+use_no_debug "Isar/runtime.ML";
use "PIDE/execution.ML";
use "ML/ml_compiler.ML";