Moving Tactic_debug to Hightactic.

8 files changed, 34 insertions, 24 deletions

diff --git a/dev/printers.mllib b/dev/printers.mllib
index a3ba42ba7..aad56f586 100644
--- a/dev/printers.mllib
+++ b/dev/printers.mllib
@@ -201,7 +201,6 @@ Egramml
 Egramcoq
 Tacsubst
 Tacenv
-Tactic_debug
 Trie
 Dn
 Btermdn
diff --git a/tactics/hightactics.mllib b/tactics/hightactics.mllib
index 468b938b6..76455f4ac 100644
--- a/tactics/hightactics.mllib
+++ b/tactics/hightactics.mllib
@@ -1,3 +1,4 @@
+Tactic_debug
 Tacintern
 Tacentries
 Tacinterp
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 6bf0e2aa7..5dab244af 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -365,7 +365,7 @@ let debugging_exception_step ist signal_anomaly e pp =
     if signal_anomaly then explain_logic_error
     else explain_logic_error_no_anomaly in
   debugging_step ist (fun () ->
-    pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ !explain_exc e)
+    pp() ++ spc() ++ str "raised the exception" ++ fnl() ++ explain_exc e)
 
 let error_ltac_variable loc id env v s =
    user_err_loc (loc, "", str "Ltac variable " ++ pr_id id ++
diff --git a/tactics/tactic_debug.ml b/tactics/tactic_debug.ml
index e991eb86d..d661f9677 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
diff --git a/tactics/tactic_debug.mli b/tactics/tactic_debug.mli
index 523398e75..520fb41ef 100644
--- a/tactics/tactic_debug.mli
+++ b/tactics/tactic_debug.mli
@@ -61,13 +61,13 @@ val db_matching_failure : debug_info -> unit Proofview.NonLogical.t
 val db_eval_failure : debug_info -> Pp.std_ppcmds -> unit Proofview.NonLogical.t
 
 (** An exception handler *)
-val explain_logic_error: (exn -> Pp.std_ppcmds) ref
+val explain_logic_error: exn -> Pp.std_ppcmds
 
 (** For use in the Ltac debugger: some exception that are usually
    consider anomalies are acceptable because they are caught later in
    the process that is being debugged.  One should not require
    from users that they report these anomalies. *)
-val explain_logic_error_no_anomaly : (exn -> Pp.std_ppcmds) ref
+val explain_logic_error_no_anomaly : exn -> Pp.std_ppcmds
 
 (** Prints a logic failure message for a rule *)
 val db_logic_failure : debug_info -> exn -> unit Proofview.NonLogical.t
diff --git a/tactics/tactics.mllib b/tactics/tactics.mllib
index b495a885f..c290ce228 100644
--- a/tactics/tactics.mllib
+++ b/tactics/tactics.mllib
@@ -20,5 +20,4 @@ Tacenv
 Hints
 Auto
 Tactic_matching
-Tactic_debug
 Term_dnet
diff --git a/toplevel/cerrors.ml b/toplevel/cerrors.ml
index 0b8edd91c..4f3ffbcae 100644
--- a/toplevel/cerrors.ml
+++ b/toplevel/cerrors.ml
@@ -110,6 +110,11 @@ let rec strip_wrapping_exceptions = function
     strip_wrapping_exceptions e
   | exc -> exc
 
+let additional_error_info = ref []
+
+let register_additional_error_info f =
+  additional_error_info := f :: !additional_error_info
+
 let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc, info) =
   let exc = strip_wrapping_exceptions exc in
   let e = process_vernac_interp_error with_header (exc, info) in
@@ -120,19 +125,12 @@ let process_vernac_interp_error ?(allow_uncaught=true) ?(with_header=true) (exc,
       let err = Errors.make_anomaly msg in
       Util.iraise (err, info)
   in
-  let ltac_trace = Exninfo.get info Tactic_debug.ltac_trace_info in
-  let loc = Option.default Loc.ghost (Loc.get_loc info) in
-  match ltac_trace with
+  let e' =
+    try Some (CList.find_map (fun f -> f e) !additional_error_info)
+    with _ -> None
+  in
+  match e' with
   | None -> e
-  | Some trace ->
-    let (e, info) = e in
-    match Tactic_debug.extract_ltac_trace trace loc with
-    | None, loc -> (e, Loc.add_loc info loc)
-    | Some msg, loc ->
-      (EvaluatedError (msg, Some e), Loc.add_loc info loc)
-
-let _ = Tactic_debug.explain_logic_error :=
-  (fun e -> Errors.print (fst (process_vernac_interp_error (e, Exninfo.null))))
-
-let _ = Tactic_debug.explain_logic_error_no_anomaly :=
-  (fun e -> Errors.print_no_report (fst (process_vernac_interp_error (e, Exninfo.null))))
+  | Some (None, loc) -> (fst e, Loc.add_loc (snd e) loc)
+  | Some (Some msg, loc) ->
+    (EvaluatedError (msg, Some (fst e)), Loc.add_loc (snd e) loc)
diff --git a/toplevel/cerrors.mli b/toplevel/cerrors.mli
index 68c46010b..a0e3e3c19 100644
--- a/toplevel/cerrors.mli
+++ b/toplevel/cerrors.mli
@@ -19,3 +19,4 @@ val process_vernac_interp_error : ?allow_uncaught:bool -> ?with_header:bool -> U
 
 val explain_exn_default : exn -> Pp.std_ppcmds
 
+val register_additional_error_info : (Util.iexn -> (Pp.std_ppcmds option * Loc.t) option) -> unit