X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_proof_checking%2FcicEnvironment.ml;h=c111acd6cf3b75d37c7301a0a90919b02051a2c9;hb=91a095f0686ee569ba035e4e30c7d071588cb8e7;hp=86b8dd921a246969fb26df7636c10ff0c5edf479;hpb=358cefe50cccd4cb7d8e2a9cecb7efcb5780b8a3;p=helm.git

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 86b8dd921..c111acd6c 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -460,7 +460,11 @@ module Cache :
      if !frozen_list <> [] then
        failwith "CicEnvironment.remove while type checking"
      else
-       HT.remove cacheOfCookedObjects uri 
+      begin
+       HT.remove cacheOfCookedObjects uri;
+       unchecked_list :=
+        List.filter (fun (uri',_) -> not (UriManager.eq uri uri')) !unchecked_list
+      end
    ;;
    
    let  list_all_cooked_uris () =
@@ -488,30 +492,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 +507,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 +533,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 +656,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