diff options
author | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-04-23 14:06:19 +0200 |
---|---|---|
committer | Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr> | 2015-04-23 14:06:19 +0200 |
commit | 0a2dfa5e5d17ccf58328432888dff345ef0bf5e6 (patch) | |
tree | 263444a0609afaac00284ad8d367eb561d4676c1 /lib/pp.ml | |
parent | 501d6dd5691474c807a722d9b5b6e3fa9d83c749 (diff) |
Removing dead code in Pp.
Diffstat (limited to 'lib/pp.ml')
-rw-r--r-- | lib/pp.ml | 21 |
1 files changed, 0 insertions, 21 deletions
@@ -18,7 +18,6 @@ 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 @@ -41,11 +40,6 @@ end = struct | GLeaf x -> f x | GNode (x,y) -> iter f x; iter f y - let rec map f = function - | GEmpty -> GEmpty - | GLeaf x -> GLeaf (f x) - | GNode (x,y) -> GNode (map f x, map f y) - end module Tag : @@ -156,21 +150,6 @@ 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) Rem 2 : if used for an iso8859_1 encoded string, the result is |