diff options
| author | Hugo Herbelin | 2016-04-09 11:56:53 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2016-04-09 18:25:59 +0200 |
| commit | ce71ac17268f11ddd92f4bea85cbdd9c62acbc21 (patch) | |
| tree | 70cd706240e86e9ecf3fe3ce1f99eee6f896381a /lib | |
| parent | bb43730ac876b8de79967090afa50f00858af6d5 (diff) | |
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.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/pp.ml | 1 | ||||
| -rw-r--r-- | lib/pp.mli | 3 |
2 files changed, 4 insertions, 0 deletions
@@ -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. *) |