(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
exception CircularDependency of string;;
exception CouldNotFreeze of string;;
exception CouldNotUnfreeze 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;;
(* ************************************************************************** *
(* ************************************************************************** *
CicParser.obj_of_xml filename bodyfilename
with exn ->
cleanup ();
CicParser.obj_of_xml filename bodyfilename
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 =
(* FIXME: decomment this when the universes will be part of the library
in
let ugraph,filename_univ =
(* FIXME: decomment this when the universes will be part of the library
| _ -> raise OnlyPutOfInductiveDefinitionsIsAllowed
;;
| _ -> 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
let add_type_checked_term uri (obj,ugraph) =
match obj with
+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
let remove_term = Cache.remove
(****************************************************************************)
exception CircularDependency of string;;
(****************************************************************************)
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
(* 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 ->
*)
val get_obj :
CicUniv.universe_graph -> UriManager.uri ->
(** Set trust function. Per default this function is set to (fun _ -> true) *)
val set_trust: (UriManager.uri -> bool) -> 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
val in_cache : UriManager.uri -> bool
+ (** @return true for objects available in the library *)
+val in_library: UriManager.uri -> bool
+