aboutsummaryrefslogtreecommitdiffhomepage
path: root/lib/pp.ml
diff options
context:
space:
mode:
authorGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-04-23 14:06:19 +0200
committerGravatar Pierre-Marie Pédrot <pierre-marie.pedrot@inria.fr>2015-04-23 14:06:19 +0200
commit0a2dfa5e5d17ccf58328432888dff345ef0bf5e6 (patch)
tree263444a0609afaac00284ad8d367eb561d4676c1 /lib/pp.ml
parent501d6dd5691474c807a722d9b5b6e3fa9d83c749 (diff)
Removing dead code in Pp.
Diffstat (limited to 'lib/pp.ml')
-rw-r--r--lib/pp.ml21
1 files changed, 0 insertions, 21 deletions
diff --git a/lib/pp.ml b/lib/pp.ml
index 6e6b32c59..d672f06db 100644
--- a/lib/pp.ml
+++ b/lib/pp.ml
@@ -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