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 d9e95a1c280aa098a4e900c923f7953e05606ae2..83dbc0e8c957966b8ea59fd10fa63527f4de75fc 100644 (file)
--- 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 a7d12f5a1611e8867d280d5df34bfd9a819665f1..c6f08afcc8c239d652e74e71b380bfc0fedd6bf8 100644 (file)
--- 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 3eb3e71593d62da04edf32dc898a1bf17b6af9c1..d46b87a59703d15bf9628f4038141b7d5b45cbcf 100644 (file)
--- 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 />