]> matita.cs.unibo.it Git - helm.git/commitdiff
Bug fixed: ls?baseuri=(cic|theory):/a/ also returned theory:/a.theory.
authorClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 26 May 2004 17:48:27 +0000 (17:48 +0000)
committerClaudio Sacerdoti Coen <claudio.sacerdoticoen@unibo.it>
Wed, 26 May 2004 17:48:27 +0000 (17:48 +0000)
helm/ocaml/getter/http_getter.ml

index cf2ee593c8ae605225f95af3c3c74a15f70beff0..6192cacdccea8f264e0fa48bc1d26b649d3019cf 100644 (file)
@@ -407,10 +407,8 @@ let ls =
     if remote () then
       ls_remote regexp
     else begin
-      let pat =
-        Pcre.replace ~rex:trailing_slash_RE ("^" ^ regexp)
-(*         (match lsuri with Cic p -> ("cic:" ^ p) | Theory p -> ("theory:" ^ p)) *)
-      in
+      let looking_for_dir = Pcre.pmatch ~rex:trailing_slash_RE regexp in
+      let pat = Pcre.replace ~rex:trailing_slash_RE ("^" ^ regexp) in
       let (dir_RE, obj_RE) =
         (Pcre.regexp (pat ^ "/"), Pcre.regexp (pat ^ "(\\.|$)"))
       in
@@ -444,13 +442,15 @@ let ls =
         (* BLEARGH Dbm module lacks support for fold-like functions *)
         (fun key _ ->
           match key with
-          | uri when Pcre.pmatch ~rex:dir_RE uri ->  (* directory hit *)
+          | uri when looking_for_dir && Pcre.pmatch ~rex:dir_RE uri ->
+              (* directory hit *)
               let localpart = Pcre.replace ~rex:dir_RE uri in
               if Pcre.pmatch ~rex:no_slashes_RE localpart then
                 store_obj localpart
               else
                 store_dir localpart
-          | uri when Pcre.pmatch ~rex:obj_RE  uri ->  (* file hit *)
+          | uri when (not looking_for_dir) && Pcre.pmatch ~rex:obj_RE  uri ->
+              (* file hit *)
               store_obj (Pcre.replace ~rex:til_slash_RE uri)
           | uri -> () (* miss *));
       let ls_items = ref [] in