X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=6192cacdccea8f264e0fa48bc1d26b649d3019cf;hb=d09e006a81595572f00eb0de7f1e954b6e20f66a;hp=1e85f70b4187fce62a50448eea3c5e192f439407;hpb=954bacdd1f1ea6a649f3bf6cd5fab4d1222f9f8f;p=helm.git

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 1e85f70b4..6192cacdc 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -30,7 +30,6 @@ open Printf
 
 open Http_getter_common
 open Http_getter_misc
-open Http_getter_debugger
 open Http_getter_types
 
 exception Not_implemented of string
@@ -81,7 +80,7 @@ let map_of_uri = function
   | uri -> raise (Unresolvable_URI uri)
 
 let update_from_server logger server_url = (* use global maps *)
-  debug_print ("Updating information from " ^ server_url);
+  Http_getter_logger.log ("Updating information from " ^ server_url);
   let xml_url_of_uri = function
       (* TODO missing sanity checks on server_url, e.g. it can contains $1 *)
     | uri when (Pcre.pmatch ~rex:heading_cic_RE uri) ->
@@ -108,7 +107,7 @@ let update_from_server logger server_url = (* use global maps *)
      http_get (server_url ^ "/" ^ (Lazy.force Http_getter_env.xsl_index)))
   in
   if (xml_index = None && rdf_index = None && xsl_index = None) then
-    debug_print (sprintf "Warning: useless server %s" server_url);
+    Http_getter_logger.log (sprintf "Warning: useless server %s" server_url);
   (match xml_index with
   | Some xml_index ->
       logger (`T "- Updating XML db ...");
@@ -171,7 +170,7 @@ let update_from_server logger server_url = (* use global maps *)
       logger (`T "All done");
       logger `BR
   | None -> ());
-  debug_print "done with this server"
+  Http_getter_logger.log "done with this server"
 
 let update_from_all_servers logger () =  (* use global maps *)
   clear_maps ();
@@ -222,8 +221,8 @@ let resolve_remote uri =
   (* deliver resolve request to http_getter *)
   let doc = ClientHTTP.get (sprintf "%sresolve?uri=%s" (getter_url ()) uri) in
   let res = ref Unknown in
-   Pxp_yacc.process_entity Pxp_yacc.default_config (`Entry_content [])
-    (Pxp_yacc.create_entity_manager ~is_document:true Pxp_yacc.default_config
+   Pxp_yacc.process_entity PxpHelmConf.pxp_config (`Entry_content [])
+    (Pxp_yacc.create_entity_manager ~is_document:true PxpHelmConf.pxp_config
      (Pxp_yacc.from_string doc))
     (function
       | Pxp_yacc.E_start_tag ("url",["value",url],_) -> res := Resolved url
@@ -395,22 +394,21 @@ let ls =
       "^([^.]*\\.[^.]*)((\\.body)|(\\.proof_tree)|(\\.types))?(\\.ann)?$"
   in
   let (types_RE, types_ann_RE, body_RE, body_ann_RE,
-       proof_tree_RE, proof_tree_ann_RE) =
+       proof_tree_RE, proof_tree_ann_RE, trailing_slash_RE) =
     (Pcre.regexp "\\.types$", Pcre.regexp "\\.types\\.ann$",
      Pcre.regexp "\\.body$", Pcre.regexp "\\.body\\.ann$",
-     Pcre.regexp "\\.proof_tree$", Pcre.regexp "\\.proof_tree\\.ann$")
+     Pcre.regexp "\\.proof_tree$", Pcre.regexp "\\.proof_tree\\.ann$",
+     Pcre.regexp "/$")
   in
   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))
-      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