- renamed Term_not_found exception (useless) with Object_not_found

[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 7845818b716777b6109287569541439240c04d40..461c3edc62f49d595cdb49fc5e82b23c0c15984e 100644 (file)
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.ml
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
@@ -59,7 +59,7 @@ exception AlreadyCooked of string;;
 exception CircularDependency of string;;
 exception CouldNotFreeze of string;;
 exception CouldNotUnfreeze of string;;
-exception Term_not_found of UriManager.uri;;
+exception Object_not_found of UriManager.uri;;
 
 
 (* ************************************************************************** *
@@ -508,7 +508,10 @@ let get_object_to_add uri =
      CicParser.obj_of_xml filename bodyfilename 
    with exn -> 
      cleanup ();
-     raise exn
+     (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 = 
    (* FIXME: decomment this when the universes will be part of the library
@@ -653,18 +656,8 @@ let put_inductive_definition uri (obj,ugraph) =
   | _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed
 ;;
 
-let in_cache uri = 
- if Cache.is_in_cooked uri then
-   (prerr_endline "TROVATO NELLA CHECKED";true)
- else  
-   if Cache.is_in_frozen uri then
-     (prerr_endline "TROVATO NELLA FROZEN";true)
-   else
-     if Cache.is_in_unchecked uri then
-       (prerr_endline "TROVATO NELLA UNCHECKED";true)
-     else
-       (prerr_endline ("NON TROVATO:" ^ (UriManager.string_of_uri uri) );false)
-;;
+let in_cache uri =
+  Cache.is_in_cooked uri || Cache.is_in_frozen uri || Cache.is_in_unchecked uri
 
 let add_type_checked_term uri (obj,ugraph) =
   match obj with 
@@ -674,5 +667,12 @@ let add_type_checked_term uri (obj,ugraph) =
        assert false 
 ;;
 
+let in_library uri =
+  in_cache uri ||
+  (try
+    ignore (Http_getter.resolve' uri);
+    true
+  with Http_getter_types.Key_not_found _ -> false)
+
 let remove_term = Cache.remove