ported to new getter interface

[helm.git] / helm / ocaml / cic_proof_checking / cicEnvironment.ml

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 86b8dd921a246969fb26df7636c10ff0c5edf479..1f2c6be0e1704662c2c92fa46c51eb43a118c004 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -488,30 +488,11 @@ let get_object_to_add uri =
     match UriManager.bodyuri_of_uri uri with
        None -> None
     |  Some bodyuri ->
-        try
-         ignore (Http_getter.resolve' bodyuri) ;
-         (* The body exists ==> it is not an axiom *)
-         Some (Http_getter.getxml' bodyuri)
-        with
-         Http_getter_types.Key_not_found _ ->
-          (* The body does not exist ==> we consider it an axiom *)
+        if Http_getter.exists' bodyuri then
+          Some (Http_getter.getxml' bodyuri)
+        else
           None
   in
-  let cleanup () =
-    Unix.unlink filename ;
-    (*
-      begin
-        match filename_univ with
-          Some f -> Unix.unlink f
-        | None -> ()
-      end;
-    *)
-    begin
-      match bodyfilename with
-          Some f -> Unix.unlink f
-        | None -> ()
-    end 
-  in
   (* restarts the numbering of named universes (the ones inside the cic) *)
   let _ = CicUniv.restart_numbering () in 
   let obj = 
@@ -522,13 +503,12 @@ let get_object_to_add uri =
         !total_parsing_time +. ((Unix.gettimeofday()) -. time );
       rc
     with exn -> 
-      cleanup ();
       (match exn with
       | CicParser.Getter_failure ("key_not_found", uri) ->
           raise (Object_not_found (UriManager.uri_of_string uri))
       | _ -> raise exn)
   in
- let ugraph,filename_univ = 
+  let ugraph,filename_univ = 
    (* FIXME: decomment this when the universes will be part of the library
     try 
       let filename_univ = 
@@ -549,10 +529,8 @@ let get_object_to_add uri =
       ***********************************************)
       (Some CicUniv.empty_ugraph,None)
   in
-    cleanup();
-    obj,ugraph
- with
-  Http_getter_types.Key_not_found _ -> raise (Object_not_found uri)
+  obj,ugraph
+ with Http_getter_types.Key_not_found _ -> raise (Object_not_found uri)
 ;;
  
 (* this is the function to fetch the object in the unchecked list and 
@@ -674,12 +652,7 @@ let in_cache uri =
 let add_type_checked_obj uri (obj,ugraph) =
  Cache.add_cooked ~key:uri (obj,ugraph)
 
-let in_library uri =
-  in_cache uri ||
-  (try
-    ignore (Http_getter.resolve' uri);
-    true
-  with Http_getter_types.Key_not_found _ -> false)
+let in_library uri = in_cache uri || Http_getter.exists' uri
 
 let remove_obj = Cache.remove