1995-08-09 08:06:35 -07:00
|
|
|
(***********************************************************************)
|
|
|
|
(* *)
|
|
|
|
(* Caml Special Light *)
|
|
|
|
(* *)
|
|
|
|
(* Xavier Leroy, projet Cristal, INRIA Rocquencourt *)
|
|
|
|
(* *)
|
|
|
|
(* Copyright 1995 Institut National de Recherche en Informatique et *)
|
|
|
|
(* Automatique. Distributed only by permission. *)
|
|
|
|
(* *)
|
|
|
|
(***********************************************************************)
|
|
|
|
|
|
|
|
(* $Id$ *)
|
|
|
|
|
1995-05-04 03:15:53 -07:00
|
|
|
let current_dir_name = "."
|
|
|
|
|
|
|
|
let concat dirname filename =
|
|
|
|
let l = String.length dirname - 1 in
|
|
|
|
if l < 0 or String.get dirname l = '/'
|
|
|
|
then dirname ^ filename
|
|
|
|
else dirname ^ "/" ^ filename
|
|
|
|
|
|
|
|
let is_absolute n =
|
|
|
|
(String.length n >= 1 & String.sub n 0 1 = "/")
|
|
|
|
or (String.length n >= 2 & String.sub n 0 2 = "./")
|
|
|
|
or (String.length n >= 3 & String.sub n 0 3 = "../")
|
|
|
|
|
1995-10-24 08:38:03 -07:00
|
|
|
let rindex s c =
|
1995-05-04 03:15:53 -07:00
|
|
|
let rec pos i =
|
|
|
|
if i < 0 then raise Not_found
|
1995-10-24 08:38:03 -07:00
|
|
|
else if String.get s i = c then i
|
1995-05-04 03:15:53 -07:00
|
|
|
else pos (i - 1)
|
|
|
|
in pos (String.length s - 1)
|
|
|
|
|
1995-10-24 08:38:03 -07:00
|
|
|
let check_suffix name suff =
|
|
|
|
String.length name >= String.length suff &
|
|
|
|
String.sub name (String.length name - String.length suff) (String.length suff)
|
|
|
|
= suff
|
|
|
|
|
|
|
|
let chop_suffix name suff =
|
|
|
|
let n = String.length name - String.length suff in
|
|
|
|
if n < 0 then invalid_arg "chop_suffix" else String.sub name 0 n
|
|
|
|
|
|
|
|
let chop_extension name =
|
|
|
|
try
|
|
|
|
String.sub name 0 (rindex name '.')
|
|
|
|
with Not_found ->
|
|
|
|
invalid_arg "Filename.chop_extension"
|
|
|
|
|
1995-05-04 03:15:53 -07:00
|
|
|
let basename name =
|
|
|
|
try
|
1995-10-24 08:38:03 -07:00
|
|
|
let p = rindex name '/' + 1 in
|
|
|
|
String.sub name p (String.length name - p)
|
1995-05-04 03:15:53 -07:00
|
|
|
with Not_found ->
|
|
|
|
name
|
|
|
|
|
|
|
|
let dirname name =
|
|
|
|
try
|
1995-10-24 08:38:03 -07:00
|
|
|
match rindex name '/' with
|
1995-05-04 03:15:53 -07:00
|
|
|
0 -> "/"
|
1995-10-24 08:38:03 -07:00
|
|
|
| n -> String.sub name 0 n
|
1995-05-04 03:15:53 -07:00
|
|
|
with Not_found ->
|
|
|
|
"."
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|