From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 6 Jul 2005 12:10:53 +0000 (+0000)
Subject: do not .body/.types/.proof_tree files from ls output
X-Git-Tag: V_0_7_1~65
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=f5ec5f0dd0b2fb5aa8ee8e2c0c734bc2c1a19955;p=helm.git

do not .body/.types/.proof_tree files from ls output
---

diff --git a/helm/ocaml/getter/http_getter.ml b/helm/ocaml/getter/http_getter.ml
index 9254c13f6..e0b948ad9 100644
--- a/helm/ocaml/getter/http_getter.ml
+++ b/helm/ocaml/getter/http_getter.ml
@@ -63,7 +63,8 @@ let pipe_RE               = Pcre.regexp "\\|"
 let til_slash_RE          = Pcre.regexp "^.*/"
 let no_slashes_RE         = Pcre.regexp "^[^/]*$"
 let fix_regexp_RE         = Pcre.regexp ("^" ^ (Pcre.quote "(cic|theory)"))
-let showable_file_RE      = Pcre.regexp "(\\.con|\\.ind|\\.var)$"
+let showable_file_RE      =
+  Pcre.regexp "(\\.con|\\.ind|\\.var|\\.body|\\.types|\\.proof_tree)$"
 
 let xml_suffix = ".xml"
 let theory_suffix = ".theory" ^ xml_suffix
@@ -155,7 +156,7 @@ let getxml uri =
     with Http_getter_storage.Resource_not_found _ -> raise (Key_not_found uri)
   end
 
-let getxslt ?(patch_dtd = true) uri = assert false
+let getxslt uri = assert false
 (* let getxslt ?(patch_dtd = true) uri =
   if remote () then
     getxslt_remote ~patch_dtd uri
@@ -190,6 +191,7 @@ let (++) (oldann, oldtypes, oldbody, oldtree)
    (if newtree  > oldtree   then newtree  else oldtree))
     
 let store_obj tbl o =
+(*   prerr_endline ("Http_getter.store_obj " ^ o); *)
   if Pcre.pmatch ~rex:showable_file_RE o then begin
     let basepart = Pcre.replace ~rex:basepart_RE ~templ:"$1" o in
     let no_flags = false, No, No, No in
@@ -230,6 +232,7 @@ let collect_ls_items dirs_set objs_tbl =
 
   (** non regexp-aware version of ls *)
 let 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
     let objs = Hashtbl.create 17 in
diff --git a/helm/ocaml/getter/http_getter.mli b/helm/ocaml/getter/http_getter.mli
index 3f56ae3da..4bbc447bd 100644
--- a/helm/ocaml/getter/http_getter.mli
+++ b/helm/ocaml/getter/http_getter.mli
@@ -45,7 +45,7 @@ val resolve: string -> string (* uri -> url *)
 val exists: string -> bool
 
 val getxml  : string -> string
-val getxslt : ?patch_dtd:bool -> string -> string
+val getxslt : string -> string
 val getdtd  : string -> string
 val clean_cache: unit -> unit
 val getalluris: unit -> string list