diff options
Diffstat (limited to 'lib')
| -rw-r--r-- | lib/envars.ml | 4 | ||||
| -rw-r--r-- | lib/util.ml | 18 | ||||
| -rw-r--r-- | lib/util.mli | 1 |
3 files changed, 14 insertions, 9 deletions
diff --git a/lib/envars.ml b/lib/envars.ml index 82e0d31622..e67fc32d94 100644 --- a/lib/envars.ml +++ b/lib/envars.ml @@ -30,8 +30,8 @@ let coqlib () = (if !Flags.boot then Coq_config.coqsrc else guess_coqlib ()) let path_to_list p = - let sep = Str.regexp_string (if Sys.os_type = "Win32" then ";" else ":") in - Str.split sep p + let sep = if Sys.os_type = "Win32" then ';' else ':' in + Util.split_string_at sep p let rec which l f = match l with diff --git a/lib/util.ml b/lib/util.ml index 6803412fdb..fe715f0a77 100644 --- a/lib/util.ml +++ b/lib/util.ml @@ -109,19 +109,23 @@ let ordinal n = (* string parsing *) -let parse_loadpath s = +let split_string_at c s = let len = String.length s in - let rec decoupe_dirs n = + let rec split n = try - let pos = String.index_from s n '/' in - if pos = n then - invalid_arg "parse_loadpath: find an empty dir in loadpath"; + let pos = String.index_from s n c in let dir = String.sub s n (pos-n) in - dir :: (decoupe_dirs (succ pos)) + dir :: split (succ pos) with | Not_found -> [String.sub s n (len-n)] in - if len = 0 then [] else decoupe_dirs 0 + if len = 0 then [] else split 0 + +let parse_loadpath s = + let l = split_string_at '/' s in + if List.mem "" l then + invalid_arg "parse_loadpath: find an empty dir in loadpath"; + l module Stringset = Set.Make(struct type t = string let compare = compare end) diff --git a/lib/util.mli b/lib/util.mli index 49e1fb4bd9..b6403fd732 100644 --- a/lib/util.mli +++ b/lib/util.mli @@ -77,6 +77,7 @@ val string_index_from : string -> int -> string -> int val string_string_contains : where:string -> what:string -> bool val plural : int -> string -> string val ordinal : int -> string +val split_string_at : char -> string -> string list val parse_loadpath : string -> string list |
