# HG changeset patch
# User wenzelm
# Date 1456944211 -3600
# Node ID 5dfcc9697f291c1865d3bd652a94b730a0350503
# Parent  5b5b704f4811c3bf6e554d4508bb88dfa3e0cac7
support for ML_exception_debugger;

diff -r 5b5b704f4811 -r 5dfcc9697f29 NEWS
--- 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
diff -r 5b5b704f4811 -r 5dfcc9697f29 etc/options
--- 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"
 
diff -r 5b5b704f4811 -r 5dfcc9697f29 src/Pure/Isar/attrib.ML
--- 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 #>
diff -r 5b5b704f4811 -r 5dfcc9697f29 src/Pure/Isar/runtime.ML
--- 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;
-
diff -r 5b5b704f4811 -r 5dfcc9697f29 src/Pure/ML/exn_debugger.ML
--- /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;
diff -r 5b5b704f4811 -r 5dfcc9697f29 src/Pure/ML/ml_options.ML
--- 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});
diff -r 5b5b704f4811 -r 5dfcc9697f29 src/Pure/ROOT
--- 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"
diff -r 5b5b704f4811 -r 5dfcc9697f29 src/Pure/ROOT.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";