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;;
(* ************************************************************************** *
val is_in_frozen: UriManager.uri -> bool
val is_in_unchecked: UriManager.uri -> bool
val is_in_cooked: UriManager.uri -> bool
+ val list_all_cooked_uris: unit -> UriManager.uri list
end
=
struct
HT.remove cacheOfCookedObjects uri
;;
+ let list_all_cooked_uris () =
+ HT.fold (fun u _ l -> u::l) cacheOfCookedObjects []
+ ;;
+
end
;;
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
| _ -> 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
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
+
+let list_uri () =
+ Cache.list_all_cooked_uris ()
+;;
+let list_obj () =
+ try
+ List.map (fun u ->
+ let o,ug = get_obj CicUniv.empty_ugraph u in
+ (u,o,ug))
+ (list_uri ())
+ with
+ Not_found ->
+ prerr_endline "Who has removed the uri in the meanwhile?";
+ raise Not_found
+;;