From 502eecdd0e3d63c7e1a647c633b588e738f0afcf Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 24 Jan 2005 16:17:33 +0000
Subject: [PATCH] - renamed Term_not_found exception (useless) with
 Object_not_found   (now used) - added getter exception handling. Now,
 hopefully, we will no longer see   Pxp_types.At exception, but more
 meaningful ones (like Object_not_found) - added in_libary which checks if an
 object exists (either in cache   or via getter) - in_cache: removed old
 debugging messages

---
 .../cic_proof_checking/cicEnvironment.ml      | 28 +++++++++----------
 .../cic_proof_checking/cicEnvironment.mli     |  9 ++++--
 2 files changed, 21 insertions(+), 16 deletions(-)

diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.ml b/helm/ocaml/cic_proof_checking/cicEnvironment.ml
index 7845818b7..461c3edc6 100644
--- 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
 
diff --git a/helm/ocaml/cic_proof_checking/cicEnvironment.mli b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
index 9875f52ac..77f97ed96 100644
--- a/helm/ocaml/cic_proof_checking/cicEnvironment.mli
+++ b/helm/ocaml/cic_proof_checking/cicEnvironment.mli
@@ -37,10 +37,11 @@
 (****************************************************************************)
 
 exception CircularDependency of string;;
-exception Term_not_found of UriManager.uri;;
+exception Object_not_found of UriManager.uri;;
 
 (* as the get cooked, but if not present the object is only fetched,
  * not unfreezed and committed 
+ * @raise Object_not_found
  *)
 val get_obj : 
   CicUniv.universe_graph -> UriManager.uri ->   
@@ -115,7 +116,11 @@ val empty : unit -> unit
 (** Set trust function. Per default this function is set to (fun _ -> true) *)
 val set_trust: (UriManager.uri -> bool) -> unit
 
-(* for filtering in tacticChaser *)
+  (** @return true for objects currently cooked/frozend/unchecked, false
+  * otherwise (i.e. objects already parsed from XML) *)
 val in_cache : UriManager.uri -> bool
 
+  (** @return true for objects available in the library *)
+val in_library: UriManager.uri -> bool
+
 (* EOF *)
-- 
2.39.2