Use streams rather than strings to handle bullet suggestions.

5 files changed, 21 insertions, 28 deletions

diff --git a/printing/printer.ml b/printing/printer.ml
index 7c031ea536..b6dda93c22 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -639,8 +639,8 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () =
 	  | _ , _, _ ->
             let end_cmd =
               str "This subproof is complete, but there are some unfocused goals." ++
-	      (match Proof_global.Bullet.suggest p
-              with None  -> str"" | Some s -> fnl () ++ str s) ++
+              (let s = Proof_global.Bullet.suggest p in
+               if Pp.is_empty s then s else fnl () ++ s) ++
               fnl ()
             in
 	    pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 8808dbbacd..22aab6585c 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -466,7 +466,7 @@ module Bullet = struct
   type behavior = {
     name : string;
     put : Proof.proof -> t -> Proof.proof;
-    suggest: Proof.proof -> string option
+    suggest: Proof.proof -> std_ppcmds
   }
 
   let behaviors = Hashtbl.create 4
@@ -476,7 +476,7 @@ module Bullet = struct
   let none = {
     name = "None";
     put = (fun x _ -> x);
-    suggest = (fun _ -> None)
+    suggest = (fun _ -> mt ())
   }
   let _ = register_behavior none
 
@@ -492,26 +492,20 @@ module Bullet = struct
     (* give a message only if more informative than the standard coq message *)
     let suggest_on_solved_goal sugg =
       match sugg with
-      | NeedClosingBrace -> Some "Try unfocusing with \"}\"."
-      | NoBulletInUse -> None
-      | ProofFinished -> None
-      | Suggest b -> Some ("Focus next goal with bullet "
-			   ^ Pp.string_of_ppcmds (pr_bullet b)
-			   ^".")
-      | Unfinished b -> Some ("The current bullet "
-			      ^ Pp.string_of_ppcmds (pr_bullet b)
-			      ^ " is unfinished.")
+      | NeedClosingBrace -> str"Try unfocusing with \"}\"."
+      | NoBulletInUse -> mt ()
+      | ProofFinished -> mt ()
+      | Suggest b -> str"Focus next goal with bullet " ++ pr_bullet b ++ str"."
+      | Unfinished b -> str"The current bullet " ++ pr_bullet b ++ str" is unfinished."
 
     (* give always a message. *)
     let suggest_on_error sugg =
       match sugg with
-      | NeedClosingBrace -> "Try unfocusing with \"}\"."
+      | NeedClosingBrace -> str"Try unfocusing with \"}\"."
       | NoBulletInUse -> assert false (* This should never raise an error. *)
-      | ProofFinished -> "No more subgoals."
-      | Suggest b -> ("Bullet " ^ Pp.string_of_ppcmds (pr_bullet b)
-		      ^ " is mandatory here.")
-      | Unfinished b -> ("Current bullet " ^ Pp.string_of_ppcmds (pr_bullet b)
-			 ^ " is not finished.")
+      | ProofFinished -> str"No more subgoals."
+      | Suggest b -> str"Bullet " ++ pr_bullet b ++ str" is mandatory here."
+      | Unfinished b -> str"Current bullet " ++ pr_bullet b ++ str" is not finished."
 
     exception FailedBullet of t * suggestion
 
@@ -519,8 +513,8 @@ module Bullet = struct
       Errors.register_handler
 	(function
 	| FailedBullet (b,sugg) ->
-	  let prefix = "Wrong bullet " ^ Pp.string_of_ppcmds (pr_bullet b) ^ " : " in
-	  Errors.errorlabstrm "Focus" (str prefix ++ str (suggest_on_error sugg))
+	  let prefix = str"Wrong bullet " ++ pr_bullet b ++ str" : " in
+	  Errors.errorlabstrm "Focus" (prefix ++ suggest_on_error sugg)
 	| _ -> raise Errors.Unhandled)
 
 
diff --git a/proofs/proof_global.mli b/proofs/proof_global.mli
index 5f11589508..5d89044c3d 100644
--- a/proofs/proof_global.mli
+++ b/proofs/proof_global.mli
@@ -172,7 +172,7 @@ module Bullet : sig
   type behavior = {
     name : string;
     put : Proof.proof -> t -> Proof.proof;
-    suggest: Proof.proof -> string option
+    suggest: Proof.proof -> Pp.std_ppcmds
   }
 
   (** A registered behavior can then be accessed in Coq
@@ -189,7 +189,7 @@ module Bullet : sig
   (** Handles focusing/defocusing with bullets:
        *)
   val put : Proof.proof -> t -> Proof.proof
-  val suggest : Proof.proof -> string option
+  val suggest : Proof.proof -> Pp.std_ppcmds
 end
 
 
diff --git a/proofs/proofview.ml b/proofs/proofview.ml
index 9ee7df14c8..e01bed5dad 100644
--- a/proofs/proofview.ml
+++ b/proofs/proofview.ml
@@ -353,7 +353,7 @@ 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 nosuchgoals_hook:(int -> std_ppcmds) ref = ref (fun n -> mt ())
 let set_nosuchgoals_hook f = nosuchgoals_hook := f
 
 
@@ -361,10 +361,9 @@ let set_nosuchgoals_hook f = nosuchgoals_hook := f
 (* This uses the hook above *)
 let _ = Errors.register_handler begin function
   | NoSuchGoals n ->
-    let suffix:string option = (!nosuchgoals_hook) n in
+    let suffix = !nosuchgoals_hook n in
     Errors.errorlabstrm ""
-      (str "No such " ++ str (String.plural n "goal") ++ str "."
-       ++ pr_opt str suffix)
+      (str "No such " ++ str (String.plural n "goal") ++ str "." ++ suffix)
   | _ -> raise Errors.Unhandled
 end
 
diff --git a/proofs/proofview.mli b/proofs/proofview.mli
index a92abcbbf1..96fe474f66 100644
--- a/proofs/proofview.mli
+++ b/proofs/proofview.mli
@@ -235,7 +235,7 @@ 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 -> string option) -> unit
+val set_nosuchgoals_hook: (int -> Pp.std_ppcmds) -> unit
 
 val tclFOCUS : int -> int -> 'a tactic -> 'a tactic