diff options
| author | Pierre-Marie Pédrot | 2016-03-20 03:10:54 +0100 |
|---|---|---|
| committer | Pierre-Marie Pédrot | 2016-03-20 21:26:40 +0100 |
| commit | f39543a752d05e5661749bbc3f221d75e525b3b4 (patch) | |
| tree | 63f0b0a9f9339a0b1e0b1086afa0346216a1f4d5 /tactics/tactic_debug.ml | |
| parent | 6afe572a4448e50f18e408097dd9ed03cc432d39 (diff) | |
Moving Tactic_debug to Hightactic.
Diffstat (limited to 'tactics/tactic_debug.ml')
| -rw-r--r-- | tactics/tactic_debug.ml | 20 |
1 files changed, 16 insertions, 4 deletions
diff --git a/tactics/tactic_debug.ml b/tactics/tactic_debug.ml index e991eb86dc..d661f9677c 100644 --- a/tactics/tactic_debug.ml +++ b/tactics/tactic_debug.ml @@ -14,6 +14,7 @@ open Termops open Nameops open Proofview.Notations + let (ltac_trace_info : ltac_trace Exninfo.t) = Exninfo.make () let prtac x = @@ -34,9 +35,11 @@ type debug_info = | DebugOff (* An exception handler *) -let explain_logic_error = ref (fun e -> mt()) +let explain_logic_error e = + Errors.print (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))) -let explain_logic_error_no_anomaly = ref (fun e -> mt()) +let explain_logic_error_no_anomaly e = + Errors.print_no_report (fst (Cerrors.process_vernac_interp_error (e, Exninfo.null))) let msg_tac_debug s = Proofview.NonLogical.print_debug (s++fnl()) let msg_tac_notice s = Proofview.NonLogical.print_notice (s++fnl()) @@ -202,7 +205,7 @@ let debug_prompt lev tac f = (Proofview.tclLIFT begin (skip:=0) >> (skipped:=0) >> if Logic.catchable_exception reraise then - msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ Pervasives.(!) explain_logic_error reraise) + msg_tac_debug (str "Level " ++ int lev ++ str ": " ++ explain_logic_error reraise) else return () end) (Proofview.tclZERO ~info reraise) @@ -304,7 +307,7 @@ let db_logic_failure debug err = is_debug debug >>= fun db -> if db then begin - msg_tac_debug (Pervasives.(!) explain_logic_error err) >> + msg_tac_debug (explain_logic_error err) >> msg_tac_debug (str "This rule has failed due to a logic error!" ++ fnl() ++ str "Let us try the next one...") end @@ -398,3 +401,12 @@ let extract_ltac_trace trace eloc = | [] -> Loc.ghost in aux trace in None, best_loc + +let get_ltac_trace (_, info) = + let ltac_trace = Exninfo.get info ltac_trace_info in + let loc = Option.default Loc.ghost (Loc.get_loc info) in + match ltac_trace with + | None -> None + | Some trace -> Some (extract_ltac_trace trace loc) + +let () = Cerrors.register_additional_error_info get_ltac_trace |