diff options
| author |  Matej Kosik <matej.kosik@inria.fr> | 2016-09-28 16:19:23 +0200 |
|---|---|---|
| committer | Matej Kosik <matej.kosik@inria.fr> | 2016-09-28 16:34:21 +0200 |
| commit | a75770eb41e8a3bbfb44cb65d04bb3af29448fe7 (patch) | |
| tree | 2de3f36abd006b58d7e4a8f89efca0a4116abaf4 /lib | |
| parent | daae678047ee2a1c53d4dc423976f77e40ba753f (diff) | |
CLEANUP: remove the definition of the "CString.map" function. We will use the official "String.map" function instead.
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/cString.ml | 7 | ||||
| -rw-r--r-- | lib/cString.mli | 3 |
2 files changed, 0 insertions, 10 deletions
diff --git a/lib/cString.ml b/lib/cString.ml index 0c2ed2e7c..61ed03083 100644 --- a/lib/cString.ml +++ b/lib/cString.ml @@ -17,7 +17,6 @@ sig val explode : string -> string list val implode : string list -> string val strip : string -> string - val map : (char -> char) -> string -> string val drop_simple_quotes : string -> string val string_index_from : string -> int -> string -> int val string_contains : where:string -> what:string -> bool @@ -78,12 +77,6 @@ let strip s = let a = lstrip_rec 0 and b = rstrip_rec (n-1) in String.sub s a (b-a+1) -let map f s = - let l = String.length s in - let r = String.create l in - for i = 0 to (l - 1) do r.[i] <- f (s.[i]) done; - r - let drop_simple_quotes s = let n = String.length s in if n > 2 && s.[0] = '\'' && s.[n-1] = '\'' then String.sub s 1 (n-2) else s diff --git a/lib/cString.mli b/lib/cString.mli index 5292b34d0..65edfbbe6 100644 --- a/lib/cString.mli +++ b/lib/cString.mli @@ -32,9 +32,6 @@ sig val strip : string -> string (** Remove the surrounding blank characters from a string *) - val map : (char -> char) -> string -> string - (** Apply a function on a string character-wise. *) - val drop_simple_quotes : string -> string (** Remove the eventual first surrounding simple quotes of a string. *) |