[proof] Fix proof bullet error helper which was implemented as a hook

We add the information on the proper layer by catching the low-level
exception.

6 files changed, 32 insertions, 31 deletions

diff --git a/engine/proofview.ml b/engine/proofview.ml
index 316f02bc37..86dcb8ab3b 100644
--- a/engine/proofview.ml
+++ b/engine/proofview.ml
@@ -345,22 +345,11 @@ 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
diff --git a/engine/proofview.mli b/engine/proofview.mli
index c772525c86..8685430c62 100644
--- a/engine/proofview.mli
+++ b/engine/proofview.mli
@@ -250,7 +250,6 @@ val tclBREAK : (iexn -> iexn option) -> 'a tactic -> 'a tactic
     This hook is used to add a suggestion about bullets when
     applicable. *)
 exception NoSuchGoals of int
-val set_nosuchgoals_hook: (int -> Pp.t) -> unit
 
 val tclFOCUS : int -> int -> 'a tactic -> 'a tactic
 
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index ef4a74b273..da3bd41bda 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -65,6 +65,13 @@ let get_current_context pf =
     let evd = Proof.in_proof p (fun x -> x) in
     evd, Global.env ()
 
+(* Improved error messages *)
+let run_tactic env tac pr =
+  try Proof.run_tactic env tac pr
+  with
+  | Proofview.NoSuchGoals i ->
+    raise Proof_bullet.(SuggestNoSuchGoals(i,pr))
+
 let solve ?with_end_tac gi info_lvl tac pr =
     let tac = match with_end_tac with
       | None -> tac
@@ -97,7 +104,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
       else tac
     in
     let env = Global.env () in
-    let (p,(status,info)) = Proof.run_tactic env tac pr in
+    let (p,(status,info)) = run_tactic env tac pr in
     let env = Global.env () in
     let sigma = Evd.from_env env in
     let () =
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml
index 2ca4f0afb4..640feb2f5b 100644
--- a/proofs/proof_bullet.ml
+++ b/proofs/proof_bullet.ml
@@ -197,3 +197,15 @@ let put p b =
 
 let suggest p =
   (!current_behavior).suggest p
+
+(* Better printing for bullet exceptions *)
+exception SuggestNoSuchGoals of int * Proof.t
+
+let _ = CErrors.register_handler begin function
+    | SuggestNoSuchGoals(n,proof) ->
+      let suffix = suggest proof in
+      CErrors.user_err
+        Pp.(str "No such " ++ str (CString.plural n "goal") ++ str "." ++
+            pr_non_empty_arg (fun x -> x) suffix)
+    | _ -> raise CErrors.Unhandled
+  end
diff --git a/proofs/proof_bullet.mli b/proofs/proof_bullet.mli
index 0fcc647a6f..6fdf818497 100644
--- a/proofs/proof_bullet.mli
+++ b/proofs/proof_bullet.mli
@@ -44,3 +44,5 @@ val register_behavior : behavior -> unit
      *)
 val put : Proof.t -> t -> Proof.t
 val suggest : Proof.t -> Pp.t
+
+exception SuggestNoSuchGoals of int * Proof.t
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 86d3d9601e..5b77b97988 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -94,6 +94,13 @@ let with_current_proof f (ps, psl) =
   let ps = { ps with proof = newpr } in
   (ps, psl), ret
 
+(* Improved error messages *)
+let with_current_proof f ((ps,_) as pf) =
+  try with_current_proof f pf
+  with
+  | Proofview.NoSuchGoals i ->
+    raise Proof_bullet.(SuggestNoSuchGoals(i,ps.proof))
+
 let simple_with_current_proof f pf =
   let p, () = with_current_proof (fun t p -> f t p , ()) pf in p
 
@@ -348,18 +355,3 @@ let update_global_env (pf : t) =
        let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in
          (p, ()))) pf
   in res
-
-(* XXX: This hook is used to provide a better error w.r.t. bullets,
-   however the proof engine [surprise!] knows nothing about bullets so
-   here we have a layering violation. The right fix is to modify the
-   entry point to handle this and reraise the exception with the
-   needed information. *)
-(* let _ =
- *   let hook n =
- *     try
- *       let prf = give_me_the_proof pf in
- *       (Proof_bullet.suggest prf)
- *     with NoCurrentProof -> mt ()
- *   in
- *   Proofview.set_nosuchgoals_hook hook *)
-