Merge remote-tracking branch 'origin/ld-0.99.3'

[helm.git] / matita / components / getter / http_getter.ml

diff --git a/matita/components/getter/http_getter.ml b/matita/components/getter/http_getter.ml
index b41c4788f2a77edfd7119b8bb49a0d89b71be622..4de03eab2e9de9caa78ab2249f7a835ca3dd9674 100644 (file)
--- a/matita/components/getter/http_getter.ml
+++ b/matita/components/getter/http_getter.ml
@@ -89,18 +89,18 @@ let getter_url () = Helm_registry.get "getter.url"
 (* Remote interface: getter methods implemented using a remote getter *)
 
   (* <TODO> *)
-let getxml_remote uri = not_implemented "getxml_remote"
-let getxslt_remote uri = not_implemented "getxslt_remote"
-let getdtd_remote uri = not_implemented "getdtd_remote"
+let getxml_remote _uri = not_implemented "getxml_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"
-let add_server_remote ~logger ~position name =
+let add_server_remote ~logger:_ ~position:_ _name =
   not_implemented "add_server_remote"
-let remove_server_remote ~logger position =
+let remove_server_remote ~logger:_ _position =
   not_implemented "remove_server_remote"
 let getalluris_remote () = not_implemented "getalluris_remote"
-let ls_remote lsuri = not_implemented "ls_remote"
-let exists_remote uri = not_implemented "exists_remote"
+let ls_remote _lsuri = not_implemented "ls_remote"
+let exists_remote _uri = not_implemented "exists_remote"
   (* </TODO> *)
 
 let resolve_remote ~writable uri =
@@ -132,7 +132,7 @@ let resolve_remote ~writable uri =
   | Exception e -> raise e
   | Resolved url -> url
 
-let deref_index_theory ~local uri =
+let deref_index_theory ~local:_ uri =
 (*  if Http_getter_storage.exists ~local (uri ^ xml_suffix) then uri *)
  if is_theory_uri uri && Filename.basename uri = "index.theory" then
     strip_trailing_slash (Filename.dirname uri) ^ theory_suffix
@@ -151,10 +151,7 @@ let exists ~local uri =
    let uri = deref_index_theory ~local uri in
     Http_getter_storage.exists ~local (uri ^ xml_suffix)
        
-let is_an_obj s = 
-  try 
-    s <> UriManager.buri_of_uri (UriManager.uri_of_string s)
-  with UriManager.IllFormedUri _ -> true
+let is_an_obj s = s <> NUri.baseuri_of_uri (NUri.uri_of_string s)
     
 let resolve ~local ~writable uri =
   if remote () then
@@ -232,7 +229,7 @@ let store_obj tbl o =
       | s when Pcre.pmatch ~rex:body_ann_RE s       -> (true,  No, Ann, No)
       | s when Pcre.pmatch ~rex:proof_tree_RE s     -> (false, No, No, Yes)
       | s when Pcre.pmatch ~rex:proof_tree_ann_RE s -> (true,  No, No, Ann)
-      | s -> no_flags
+      | _s -> no_flags
     in
     Hashtbl.replace tbl basepart (oldflags ++ newflags)
   end
@@ -363,13 +360,13 @@ let getalluris () =
 
 (* Shorthands from now on *)
 
-let getxml' uri = getxml (UriManager.string_of_uri uri)
+let getxml' uri = getxml (NUri.string_of_uri uri)
 let resolve' ~local ~writable uri =
-  resolve ~local ~writable (UriManager.string_of_uri uri)
+  resolve ~local ~writable (NUri.string_of_uri uri)
 ;;
-let exists' ~local uri = exists ~local (UriManager.string_of_uri uri)
+let exists' ~local uri = exists ~local (NUri.string_of_uri uri)
 let filename' ~local ~writable uri =
-  filename ~local ~writable (UriManager.string_of_uri uri)
+  filename ~local ~writable (NUri.string_of_uri uri)
 ;;
 
 let tilde_expand_key k =