From ce71ac17268f11ddd92f4bea85cbdd9c62acbc21 Mon Sep 17 00:00:00 2001
From: Hugo Herbelin
Date: Sat, 9 Apr 2016 11:56:53 +0200
Subject: In pr_clauses, do not print a leading space by default so that it can
 be used in the generic printer for tactics.

Allows e.g. to print "symmetry in H" correctly after its move to
TACTIC EXTEND.
---
 lib/pp.ml  | 1 +
 lib/pp.mli | 3 +++
 2 files changed, 4 insertions(+)

(limited to 'lib')

diff --git a/lib/pp.ml b/lib/pp.ml
index 9a833ae225..c7cf9b8d0e 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -518,6 +518,7 @@ let pr_comma () = str "," ++ spc ()
 let pr_semicolon () = str ";" ++ spc ()
 let pr_bar () = str "|" ++ spc ()
 let pr_arg pr x = spc () ++ pr x
+let pr_non_empty_arg pr x = let pp = pr x in if ismt pp then mt () else spc () ++ pr x
 let pr_opt pr = function None -> mt () | Some x -> pr_arg pr x
 let pr_opt_no_spc pr = function None -> mt () | Some x -> pr x
 
diff --git a/lib/pp.mli b/lib/pp.mli
index 015151bc90..2e4d029749 100644
--- a/lib/pp.mli
+++ b/lib/pp.mli
@@ -199,6 +199,9 @@ val pr_bar : unit -> std_ppcmds
 val pr_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
 (** Adds a space in front of its argument. *)
 
+val pr_non_empty_arg : ('a -> std_ppcmds) -> 'a -> std_ppcmds
+(** Adds a space in front of its argument if non empty. *)
+
 val pr_opt : ('a -> std_ppcmds) -> 'a option -> std_ppcmds
 (** Inner object preceded with a space if [Some], nothing otherwise. *)
 
-- 
cgit v1.2.3