support for ML_exception_debugger;
authorwenzelm
Wed Mar 02 19:43:31 2016 +0100 (2016-03-02)
changeset 624985dfcc9697f29
parent 62497 5b5b704f4811
child 62499 4a5b81ff5992
child 62501 98fa1f9a292f
support for ML_exception_debugger;
NEWS
etc/options
src/Pure/Isar/attrib.ML
src/Pure/Isar/runtime.ML
src/Pure/ML/exn_debugger.ML
src/Pure/ML/ml_options.ML
src/Pure/ROOT
src/Pure/ROOT.ML
     1.1 --- a/NEWS	Wed Mar 02 10:02:12 2016 +0100
     1.2 +++ b/NEWS	Wed Mar 02 19:43:31 2016 +0100
     1.3 @@ -181,6 +181,15 @@
     1.4  * Session HOL-NSA has been renamed to HOL-Nonstandard_Analysis.
     1.5  
     1.6  
     1.7 +*** ML ***
     1.8 +
     1.9 +* Option ML_exception_debugger controls detailed exception trace via the
    1.10 +Poly/ML debugger. Relevant ML modules need to be compiled beforehand
    1.11 +with ML_file_debug, or with ML_file and option ML_debugger enabled. Note
    1.12 +debugger information requires consirable time and space: main
    1.13 +Isabelle/HOL with full debugger support may need ML_system_64.
    1.14 +
    1.15 +
    1.16  *** System ***
    1.17  
    1.18  * The Isabelle system environment always ensures that the main
     2.1 --- a/etc/options	Wed Mar 02 10:02:12 2016 +0100
     2.2 +++ b/etc/options	Wed Mar 02 19:43:31 2016 +0100
     2.3 @@ -107,6 +107,9 @@
     2.4  public option ML_exception_trace : bool = false
     2.5    -- "ML exception trace for toplevel command execution"
     2.6  
     2.7 +public option ML_exception_debugger : bool = false
     2.8 +  -- "ML debugger exception trace for toplevel command execution"
     2.9 +
    2.10  public option ML_debugger : bool = false
    2.11    -- "ML debugger instrumentation for newly compiled code"
    2.12  
     3.1 --- a/src/Pure/Isar/attrib.ML	Wed Mar 02 10:02:12 2016 +0100
     3.2 +++ b/src/Pure/Isar/attrib.ML	Wed Mar 02 19:43:31 2016 +0100
     3.3 @@ -519,6 +519,7 @@
     3.4    register_config Name_Space.names_unique_raw #>
     3.5    register_config ML_Options.source_trace_raw #>
     3.6    register_config ML_Options.exception_trace_raw #>
     3.7 +  register_config ML_Options.exception_debugger_raw #>
     3.8    register_config ML_Options.debugger_raw #>
     3.9    register_config ML_Options.print_depth_raw #>
    3.10    register_config Proof_Context.show_abbrevs_raw #>
     4.1 --- a/src/Pure/Isar/runtime.ML	Wed Mar 02 10:02:12 2016 +0100
     4.2 +++ b/src/Pure/Isar/runtime.ML	Wed Mar 02 19:43:31 2016 +0100
     4.3 @@ -19,6 +19,8 @@
     4.4    val exn_system_message: exn -> unit
     4.5    val exn_trace: (unit -> 'a) -> 'a
     4.6    val exn_trace_system: (unit -> 'a) -> 'a
     4.7 +  val exn_debugger: (unit -> 'a) -> 'a
     4.8 +  val exn_debugger_system: (unit -> 'a) -> 'a
     4.9    val debugging: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    4.10    val controlled_execution: Context.generic option -> ('a -> 'b) -> 'a -> 'b
    4.11    val toplevel_error: (exn -> unit) -> ('a -> 'b) -> 'a -> 'b
    4.12 @@ -143,13 +145,45 @@
    4.13  fun exn_trace_system e = print_exception_trace exn_message Output.system_message e;
    4.14  
    4.15  
    4.16 +(* exception debugger *)
    4.17 +
    4.18 +local
    4.19 +
    4.20 +fun print_entry (name, loc) =
    4.21 +  Markup.markup Markup.item (name ^ Position.here (Exn_Properties.position_of loc));
    4.22 +
    4.23 +fun exception_debugger output e =
    4.24 +  let
    4.25 +    val (trace, result) = Exn_Debugger.capture_exception_trace e;
    4.26 +    val _ =
    4.27 +      (case (trace, result) of
    4.28 +        (_ :: _, Exn.Exn exn) =>
    4.29 +          output (cat_lines ("Exception trace - " ^ exn_message exn :: map print_entry trace))
    4.30 +      | _ => ());
    4.31 +  in Exn.release result end;
    4.32 +
    4.33 +in
    4.34 +
    4.35 +fun exn_debugger e = exception_debugger tracing e;
    4.36 +fun exn_debugger_system e = exception_debugger Output.system_message e;
    4.37 +
    4.38 +end;
    4.39 +
    4.40 +
    4.41  
    4.42  (** controlled execution **)
    4.43  
    4.44 -fun debugging opt_context f x =
    4.45 +fun debugging1 opt_context f x =
    4.46    if ML_Options.exception_trace_enabled opt_context
    4.47    then exn_trace (fn () => f x) else f x;
    4.48  
    4.49 +fun debugging2 opt_context f x =
    4.50 +  if ML_Options.exception_debugger_enabled opt_context
    4.51 +  then exn_debugger (fn () => f x) else f x;
    4.52 +
    4.53 +fun debugging opt_context f =
    4.54 +  f |> debugging1 opt_context |> debugging2 opt_context;
    4.55 +
    4.56  fun controlled_execution opt_context f x =
    4.57    (f |> debugging opt_context |> Future.interruptible_task) x;
    4.58  
    4.59 @@ -169,4 +203,3 @@
    4.60    (body |> controlled_execution NONE |> toplevel_error exn_error_message) ();
    4.61  
    4.62  end;
    4.63 -
     5.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     5.2 +++ b/src/Pure/ML/exn_debugger.ML	Wed Mar 02 19:43:31 2016 +0100
     5.3 @@ -0,0 +1,63 @@
     5.4 +(*  Title:      Pure/ML/exn_debugger.ML
     5.5 +    Author:     Makarius
     5.6 +
     5.7 +Detailed exception trace via ML debugger.
     5.8 +*)
     5.9 +
    5.10 +signature EXN_DEBUGGER =
    5.11 +sig
    5.12 +  val capture_exception_trace: (unit -> 'a) -> (string * ML_Debugger.location) list * 'a Exn.result
    5.13 +end;
    5.14 +
    5.15 +structure Exn_Debugger: EXN_DEBUGGER =
    5.16 +struct
    5.17 +
    5.18 +(* thread data *)
    5.19 +
    5.20 +local
    5.21 +  val tag = Universal.tag () : ((string * ML_Debugger.location) * exn) list option Universal.tag;
    5.22 +in
    5.23 +
    5.24 +fun start_trace () = Thread.setLocal (tag, SOME []);
    5.25 +
    5.26 +fun update_trace entry exn =
    5.27 +  (case Thread.getLocal tag of
    5.28 +    SOME (SOME trace) => Thread.setLocal (tag, SOME ((entry, exn) :: trace))
    5.29 +  | _ => ());
    5.30 +
    5.31 +fun stop_trace () =
    5.32 +  let
    5.33 +    val trace = (case Thread.getLocal tag of SOME (SOME trace) => trace | _ => []);
    5.34 +    val _ = Thread.setLocal (tag, NONE);
    5.35 +  in trace end;
    5.36 +
    5.37 +val _ = ML_Debugger.on_exit_exception (SOME update_trace);
    5.38 +
    5.39 +end;
    5.40 +
    5.41 +
    5.42 +(* capture exception trace *)
    5.43 +
    5.44 +local
    5.45 +  fun eq_exn exns =
    5.46 +    op = (apply2 General.exnName exns) andalso op = (apply2 Exn_Output.position exns);
    5.47 +in
    5.48 +
    5.49 +fun capture_exception_trace e =
    5.50 +  uninterruptible (fn restore_attributes => fn () =>
    5.51 +    let
    5.52 +      val _ = start_trace ();
    5.53 +      val result = Exn.interruptible_capture (restore_attributes e) ();
    5.54 +      val trace = stop_trace ();
    5.55 +      val trace' =
    5.56 +        (case result of
    5.57 +          Exn.Res _ => []
    5.58 +        | Exn.Exn exn =>
    5.59 +            trace
    5.60 +            |> map_filter (fn (entry, e) => if eq_exn (exn, e) then SOME entry else NONE)
    5.61 +            |> rev);
    5.62 +    in (trace', result) end) ();
    5.63 +
    5.64 +end;
    5.65 +
    5.66 +end;
     6.1 --- a/src/Pure/ML/ml_options.ML	Wed Mar 02 10:02:12 2016 +0100
     6.2 +++ b/src/Pure/ML/ml_options.ML	Wed Mar 02 19:43:31 2016 +0100
     6.3 @@ -11,6 +11,9 @@
     6.4    val exception_trace_raw: Config.raw
     6.5    val exception_trace: bool Config.T
     6.6    val exception_trace_enabled: Context.generic option -> bool
     6.7 +  val exception_debugger_raw: Config.raw
     6.8 +  val exception_debugger: bool Config.T
     6.9 +  val exception_debugger_enabled: Context.generic option -> bool
    6.10    val debugger_raw: Config.raw
    6.11    val debugger: bool Config.T
    6.12    val debugger_enabled: Context.generic option -> bool
    6.13 @@ -40,6 +43,16 @@
    6.14    | exception_trace_enabled (SOME context) = Config.get_generic context exception_trace;
    6.15  
    6.16  
    6.17 +(* exception debugger *)
    6.18 +
    6.19 +val exception_debugger_raw = Config.declare_option ("ML_exception_debugger", @{here});
    6.20 +val exception_debugger = Config.bool exception_debugger_raw;
    6.21 +
    6.22 +fun exception_debugger_enabled NONE =
    6.23 +      (Options.default_bool (Config.name_of exception_debugger_raw) handle ERROR _ => false)
    6.24 +  | exception_debugger_enabled (SOME context) = Config.get_generic context exception_debugger;
    6.25 +
    6.26 +
    6.27  (* debugger *)
    6.28  
    6.29  val debugger_raw = Config.declare_option ("ML_debugger", @{here});
     7.1 --- a/src/Pure/ROOT	Wed Mar 02 10:02:12 2016 +0100
     7.2 +++ b/src/Pure/ROOT	Wed Mar 02 19:43:31 2016 +0100
     7.3 @@ -157,6 +157,7 @@
     7.4      "Isar/token.ML"
     7.5      "Isar/toplevel.ML"
     7.6      "Isar/typedecl.ML"
     7.7 +    "ML/exn_debugger.ML"
     7.8      "ML/exn_output.ML"
     7.9      "ML/exn_properties.ML"
    7.10      "ML/install_pp_polyml.ML"
     8.1 --- a/src/Pure/ROOT.ML	Wed Mar 02 10:02:12 2016 +0100
     8.2 +++ b/src/Pure/ROOT.ML	Wed Mar 02 19:43:31 2016 +0100
     8.3 @@ -190,8 +190,9 @@
     8.4  use "ML/ml_env.ML";
     8.5  use "ML/ml_options.ML";
     8.6  use "ML/exn_output.ML";
     8.7 +use_no_debug "ML/exn_debugger.ML";
     8.8  use "ML/ml_options.ML";
     8.9 -use "Isar/runtime.ML";
    8.10 +use_no_debug "Isar/runtime.ML";
    8.11  use "PIDE/execution.ML";
    8.12  use "ML/ml_compiler.ML";
    8.13