]> matita.cs.unibo.it Git - helm.git/blobdiff - components/extlib/hExtlib.ml
some work on making the compiler command line cleaner,
[helm.git] / components / extlib / hExtlib.ml
index c32ed0bed9b5d6daac98063553aa56e50445de70..53d8c74e878b4f511877116160a4a74661a29a29 100644 (file)
@@ -452,15 +452,26 @@ let find_in paths path =
      raise 
        (Failure "find_in")
 ;;
-       
+
+let is_prefix_of_aux d1 d2 = 
+  let len1 = String.length d1 in
+  let len2 = String.length d2 in
+  if len2 < len1 then 
+    false, len1, len2
+  else
+    let pref = String.sub d2 0 len1 in
+    pref = d1 && (len1 = len2 || d1.[len1-1] = '/' || d2.[len1] = '/'), len1, len2
+
 let is_prefix_of d1 d2 =
-    let len1 = String.length d1 in
-    let len2 = String.length d2 in
-    if len2 < len1 then 
-      false
-    else
-      let pref = String.sub d2 0 len1 in
-      pref = d1 && (len1 = len2 || d2.[len1] = '/')
+  let b,_,_ = is_prefix_of_aux d1 d2 in b
+;;
+
+let chop_prefix prefix s =
+  let b,lp,ls = is_prefix_of_aux prefix s in
+  if b then
+    String.sub s lp (ls - lp)
+  else 
+    s
 ;;
 
 let touch s =