From b92fff621cce1576c93fab9276fb41ea85e10982 Mon Sep 17 00:00:00 2001
From: Pierre Courtieu
Date: Thu, 8 Jan 2015 16:59:47 +0100
Subject: Fixed and extend bullet related info/error messages. + doc.

Had to put some hook in the handler of Proofview.NoSuchgoals.
Documentation updated. CHANGE updated.
---
 proofs/proofview.ml | 16 +++++++++++++++-
 1 file changed, 15 insertions(+), 1 deletion(-)

(limited to 'proofs/proofview.ml')

diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index f1d10bbe55..44bf652125 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -343,8 +343,22 @@ let tclBREAK = Proof.break
 (** {7 Focusing tactics} *)
 
 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 -> string option) ref = ref ((fun n -> None))
+let set_nosuchgoals_hook f = nosuchgoals_hook := f
+
+
+
+(* This uses the hook above *)
 let _ = Errors.register_handler begin function
-  | NoSuchGoals n -> Errors.error ("No such " ^ String.plural n "goal" ^".")
+  | NoSuchGoals n ->
+    let suffix:string option = (!nosuchgoals_hook) n in
+    Errors.errorlabstrm ""
+      (str "No such " ++ str (String.plural n "goal") ++ str "."
+       ++ pr_opt str suffix)
   | _ -> raise Errors.Unhandled
 end
 
-- 
cgit v1.2.3