diff options
author | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 11:51:52 +0100 |
---|---|---|
committer | Regis-Gianas <yrg@pps.univ-paris-diderot.fr> | 2014-11-04 22:51:36 +0100 |
commit | 970725685ee7ecb03fa071e94695988f2b14bd90 (patch) | |
tree | dc66c8bdbd34f3362a5f92272749e5aba16da1eb /lib | |
parent | 31ce91dd0a7cf1d780bb7bc1ab4550e0270a4bcd (diff) |
lib/Pp.rewrite: New.
Allow strings of a pretty-print to be rewritten just before the
actual output.
Diffstat (limited to 'lib')
-rw-r--r-- | lib/pp.ml | 18 | ||||
-rw-r--r-- | lib/pp.mli | 3 |
2 files changed, 20 insertions, 1 deletions
@@ -22,6 +22,7 @@ module Glue : sig val empty : 'a t val is_empty : 'a t -> bool val iter : ('a -> unit) -> 'a t -> unit + val map : ('a -> 'b) -> 'a t -> 'b t end = struct @@ -33,7 +34,7 @@ end = struct let is_empty x = x = [] let iter f g = List.iter f (List.rev g) - + let map = List.map end open Pp_control @@ -115,6 +116,20 @@ let app = Glue.glue let is_empty g = Glue.is_empty g +let rewrite f p = + let strtoken = function + | Str_len (s, n) -> + let s' = f s in + Str_len (s', String.length s') + | Str_def s -> + Str_def (f s) + in + let rec ppcmd_token = function + | Ppcmd_print x -> Ppcmd_print (strtoken x) + | Ppcmd_box (bt, g) -> Ppcmd_box (bt, Glue.map ppcmd_token g) + | p -> p + in + Glue.map ppcmd_token p (* Compute length of an UTF-8 encoded string Rem 1 : utf8_length <= String.length (equal if pure ascii) @@ -309,6 +324,7 @@ let pp_dirs ft = raise reraise + (* pretty print on stdout and stderr *) (* Special chars for emacs, to detect warnings inside goal output *) diff --git a/lib/pp.mli b/lib/pp.mli index dad4ed6ab..eb847189a 100644 --- a/lib/pp.mli +++ b/lib/pp.mli @@ -46,6 +46,9 @@ val eval_ppcmds : std_ppcmds -> std_ppcmds val is_empty : std_ppcmds -> bool (** Test emptyness. *) +val rewrite : (string -> string) -> std_ppcmds -> std_ppcmds +(** [rewrite f pps] applies [f] to all strings that appear in [pps]. *) + (** {6 Derived commands} *) val spc : unit -> std_ppcmds |