X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fgetter%2Fhttp_getter.ml;h=191117a20e38c182d3af6a43824cf8c27af198af;hb=4167cea65ca58897d1a3dbb81ff95de5074700cc;hp=e0b948ad9167c0c01db237a2bc0b321c0602d380;hpb=f5ec5f0dd0b2fb5aa8ee8e2c0c734bc2c1a19955;p=helm.git

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index e0b948ad9..191117a20 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -67,7 +67,7 @@ let showable_file_RE      =
   Pcre.regexp "(\\.con|\\.ind|\\.var|\\.body|\\.types|\\.proof_tree)$"
 
 let xml_suffix = ".xml"
-let theory_suffix = ".theory" ^ xml_suffix
+let theory_suffix = ".theory"
 
   (* global maps, shared by all threads *)
 
@@ -88,7 +88,7 @@ let getter_url () = Helm_registry.get "getter.url"
 
   (* <TODO> *)
 let getxml_remote uri = not_implemented "getxml_remote"
-let getxslt_remote ~patch_dtd uri = not_implemented "getxslt_remote"
+let getxslt_remote uri = not_implemented "getxslt_remote"
 let getdtd_remote uri = not_implemented "getdtd_remote"
 let clean_cache_remote () = not_implemented "clean_cache_remote"
 let list_servers_remote () = not_implemented "list_servers_remote"
@@ -129,44 +129,46 @@ let resolve_remote uri =
   | Exception e -> raise e
   | Resolved url -> url
 
+let deref_index_theory uri =
+ if Http_getter_storage.exists (uri ^ xml_suffix) then uri
+ else if is_theory_uri uri && Filename.basename uri = "index.theory" then
+    strip_trailing_slash (Filename.dirname uri) ^ theory_suffix
+ else
+    uri
+
 (* API *)
 
 let help () = Http_getter_const.usage_string (Http_getter_env.env_to_string ())
 
 let exists uri =
+(*   prerr_endline ("Http_getter.exists " ^ uri); *)
   if remote () then
     exists_remote uri
   else
+   let uri = deref_index_theory uri in
     Http_getter_storage.exists (uri ^ xml_suffix)
 	
 let resolve uri =
   if remote () then
     resolve_remote uri
   else
+   let uri = deref_index_theory uri in
     try
       Http_getter_storage.resolve (uri ^ xml_suffix)
     with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
 
 let getxml uri =
-  if remote () then
-    getxml_remote uri
+  if remote () then getxml_remote uri
   else begin
-    try
-      Http_getter_storage.filename (uri ^ xml_suffix)
-    with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
+    let uri' = deref_index_theory uri in
+    (try
+      Http_getter_storage.filename (uri' ^ xml_suffix)
+    with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri))
   end
 
-let getxslt uri = assert false
-(* let getxslt ?(patch_dtd = true) uri =
-  if remote () then
-    getxslt_remote ~patch_dtd uri
-  else begin
-    let url = resolve uri in
-    let (fname, outchan) = temp_file_of_uri uri in
-    Http_getter_cache.respond_xsl ~via_http:false ~url ~patch:patch_dtd outchan;
-    close_out outchan;
-    fname
-  end *)
+let getxslt uri =
+  if remote () then getxslt_remote uri
+  else Http_getter_storage.filename ~find:true ("xslt:/" ^ uri)
 
 let getdtd uri =
   if remote () then
@@ -230,8 +232,10 @@ let collect_ls_items dirs_set objs_tbl =
     objs_tbl;
   List.rev !items
 
+let contains_object = (<>) []
+
   (** non regexp-aware version of ls *)
-let dumb_ls uri_prefix =
+let rec dumb_ls uri_prefix =
 (*   prerr_endline ("Http_getter.dumb_ls " ^ uri_prefix); *)
   if is_cic_obj_uri uri_prefix then begin
     let dirs = ref StringSet.empty in
@@ -248,23 +252,41 @@ let dumb_ls uri_prefix =
     collect_ls_items !dirs objs
   end else if is_theory_uri uri_prefix then begin
     let items = ref [] in
+    let add_theory fname =
+      items :=
+        Ls_object {
+          uri = fname; ann = false; types = No; body = No; proof_tree = No }
+        :: !items
+    in
+    let cic_uri_prefix =
+      Pcre.replace_first ~rex:heading_theory_RE ~templ:"cic:" uri_prefix
+    in
     List.iter
       (fun fname ->
         if ends_with_slash fname then
           items := Ls_section (strip_trailing_slash fname) :: !items
         else
           try
-            let obj =
-              { uri = strip_suffix theory_suffix fname;
-                ann = false; types = No; body = No; proof_tree = No }
-            in
-            items := Ls_object obj :: !items
+            let fname = strip_suffix ~suffix:xml_suffix fname in
+            let theory_name = strip_suffix ~suffix:theory_suffix fname in
+            let sub_theory = normalize_dir cic_uri_prefix ^ theory_name ^ "/" in
+            if is_empty_theory sub_theory then add_theory fname
           with Invalid_argument _ -> ())
       (Http_getter_storage.ls uri_prefix);
+    (try
+      if contains_object (dumb_ls cic_uri_prefix)
+        && exists (strip_trailing_slash uri_prefix ^ theory_suffix)
+      then
+        add_theory "index.theory";
+    with Unresolvable_URI _ -> ());
     !items
   end else
     raise (Invalid_URI uri_prefix)
 
+and is_empty_theory uri_prefix =
+(*   prerr_endline ("is_empty_theory " ^ uri_prefix); *)
+  not (contains_object (dumb_ls uri_prefix))
+
   (* handle simple regular expressions of the form "...(..|..|..)..." on cic
    * uris, not meant to be a real implementation of regexp. The only we use is
    * "(cic|theory):/..." *)
@@ -324,7 +346,13 @@ let getxml' uri = getxml (UriManager.string_of_uri uri)
 let resolve' uri = resolve (UriManager.string_of_uri uri)
 let exists' uri = exists (UriManager.string_of_uri uri)
 
+let tilde_expand_key k =
+  try
+    Helm_registry.set k (HExtlib.tilde_expand (Helm_registry.get k))
+  with Helm_registry.Key_not_found _ -> ()
+
 let init () =
+  List.iter tilde_expand_key ["getter.cache_dir"; "getter.dtd_dir"];
   Http_getter_logger.set_log_level
     (Helm_registry.get_opt_default Helm_registry.int ~default:1
       "getter.log_level");