From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 26 May 2004 15:29:42 +0000 (+0000)
Subject: changed /ls method so that regular expressions are used instead of plain
X-Git-Tag: pre_subst_in_kernel~82
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f82bff515257cee1dd485b251763ea4a8d5ca0e2;p=helm.git

changed /ls method so that regular expressions are used instead of plain
URIs
---

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index d9e95a1c2..83dbc0e8c 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -402,13 +402,13 @@ let ls =
   let (slash_RE, til_slash_RE, no_slashes_RE) =
     (Pcre.regexp "/", Pcre.regexp "^.*/", Pcre.regexp "^[^/]*$")
   in
-  fun lsuri ->
+  fun regexp ->
     if remote () then
-      ls_remote lsuri
+      ls_remote regexp
     else begin
       let pat =
-        "^" ^
-        (match lsuri with Cic p -> ("cic:" ^ p) | Theory p -> ("theory:" ^ p))
+        "^" ^ regexp
+(*         (match lsuri with Cic p -> ("cic:" ^ p) | Theory p -> ("theory:" ^ p)) *)
       in
       let (dir_RE, obj_RE) =
         (Pcre.regexp (pat ^ "/"), Pcre.regexp (pat ^ "(\\.|$)"))
diff --git a/helm/ocaml/getter/http_getter.mli b/helm/ocaml/getter/http_getter.mli
index a7d12f5a1..c6f08afcc 100644
--- a/helm/ocaml/getter/http_getter.mli
+++ b/helm/ocaml/getter/http_getter.mli
@@ -49,7 +49,9 @@ val add_server: ?logger:logger_callback -> ?position:int -> string -> unit
 val remove_server: ?logger:logger_callback -> int -> unit
 val getalluris: unit -> string list
 val getallrdfuris: [ `Forward | `Backward ] -> string list
-val ls: xml_uri -> ls_item list
+
+  (** @param regexp regular expression (PCRE syntax) over HELM URIs *)
+val ls: string -> ls_item list
 
   (** {2 Shorthands} *)
 
diff --git a/helm/ocaml/getter/http_getter_const.ml b/helm/ocaml/getter/http_getter_const.ml
index 3eb3e7159..d46b87a59 100644
--- a/helm/ocaml/getter/http_getter_const.ml
+++ b/helm/ocaml/getter/http_getter_const.ml
@@ -89,7 +89,7 @@ let usage_string configuration =
       <b><kbd><a href=\"/getallrdfuris\">getallrdfuris</a></kbd></b><br />
     </p>
     <p>
-      <b><kbd>ls?baseuri=URI&format=(txt|xml)</kbd></b><br />
+      <b><kbd>ls?baseuri=regexp&format=(txt|xml)</kbd></b><br />
     </p>
     <p>
       <b><kbd><a href=\"/getempty\">getempty</a></kbd></b><br />