lib/Pp.rewrite: New.

  Allow strings of a pretty-print to be rewritten just before the
  actual output.

1 files changed, 17 insertions, 1 deletions

diff --git a/lib/pp.ml b/lib/pp.ml
index dff0fb0adb..b8935f54dc 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -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 *)