From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Mon, 24 Jan 2005 16:17:33 +0000 (+0000)
Subject: - renamed Term_not_found exception (useless) with Object_not_found
X-Git-Tag: V_0_1_0~95
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=502eecdd0e3d63c7e1a647c633b588e738f0afcf;p=helm.git

- 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
---

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 *)