[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.

4 files changed, 29 insertions, 16 deletions

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 *)
-