Merge PR #9646: [proof] Fix proof bullet error helper which was implemented as a hook

Ack-by: SkySkimmer
Reviewed-by: Zimmi48
Ack-by: ejgallego

1 files changed, 11 insertions, 22 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 316f02bc37..f278c83912 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -345,29 +345,19 @@ let tclBREAK = Proof.break
 
 exception NoSuchGoals of int
 
-(* This hook returns a string to be appended to the usual message.
-   Primarily used to add a suggestion about the right bullet to use to
-   focus the next goal, if applicable. *)
-let nosuchgoals_hook:(int -> Pp.t) ref = ref (fun n -> mt ())
-let set_nosuchgoals_hook f = nosuchgoals_hook := f
-
-
-
-(* This uses the hook above *)
 let _ = CErrors.register_handler begin function
   | NoSuchGoals n ->
-    let suffix = !nosuchgoals_hook n in
-    CErrors.user_err 
-      (str "No such " ++ str (String.plural n "goal") ++ str "." ++
-       pr_non_empty_arg (fun x -> x) suffix)
-      | _ -> raise CErrors.Unhandled
+    CErrors.user_err
+      (str "No such " ++ str (String.plural n "goal") ++ str ".")
+  | _ -> raise CErrors.Unhandled
 end
 
-(** [tclFOCUS_gen nosuchgoal i j t] applies [t] in a context where
+(** [tclFOCUS ?nosuchgoal i j t] applies [t] in a context where
     only the goals numbered [i] to [j] are focused (the rest of the goals
     is restored at the end of the tactic). If the range [i]-[j] is not
     valid, then it [tclFOCUS_gen nosuchgoal i j t] is [nosuchgoal]. *)
-let tclFOCUS_gen nosuchgoal i j t =
+let tclFOCUS ?nosuchgoal i j t =
+  let nosuchgoal = Option.default (tclZERO (NoSuchGoals (j+1-i))) nosuchgoal in
   let open Proof in
   Pv.get >>= fun initial ->
   try
@@ -378,10 +368,9 @@ let tclFOCUS_gen nosuchgoal i j t =
     return result
   with CList.IndexOutOfRange -> nosuchgoal
 
-let tclFOCUS i j t = tclFOCUS_gen (tclZERO (NoSuchGoals (j+1-i))) i j t
-let tclTRYFOCUS i j t = tclFOCUS_gen (tclUNIT ()) i j t
+let tclTRYFOCUS i j t = tclFOCUS ~nosuchgoal:(tclUNIT ()) i j t
 
-let tclFOCUSLIST l t =
+let tclFOCUSLIST ?(nosuchgoal=tclZERO (NoSuchGoals 0)) l t =
   let open Proof in
   Comb.get >>= fun comb ->
     let n = CList.length comb in
@@ -395,7 +384,7 @@ let tclFOCUSLIST l t =
     in
     let l = CList.map_filter sanitize l in
     match l with
-      | [] -> tclZERO (NoSuchGoals 0)
+      | [] -> nosuchgoal
       | (mi, _) :: _ ->
           (* Get the left-most goal to focus. This goal won't move, and we
              will then place all the other goals to focus to the right. *)
@@ -412,7 +401,7 @@ let tclFOCUSLIST l t =
 
 
 (** Like {!tclFOCUS} but selects a single goal by name. *)
-let tclFOCUSID id t =
+let tclFOCUSID ?(nosuchgoal=tclZERO (NoSuchGoals 1)) id t =
   let open Proof in
   Pv.get >>= fun initial ->
   try
@@ -432,7 +421,7 @@ let tclFOCUSID id t =
         t >>= fun result ->
       Comb.set initial.comb  >>
         return result
-  with Not_found -> tclZERO (NoSuchGoals 1)
+  with Not_found -> nosuchgoal
 
 (** {7 Dispatching on goals} *)