From f3ac2308f8ed6f9a02df6e78a804cdbf54a62cea Mon Sep 17 00:00:00 2001 From: fbesson Date: Thu, 20 Aug 2009 09:13:31 +0000 Subject: new csdp cache + improved error message git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@12286 85f007b7-540e-0410-9357-904b9bb8a0f7 --- plugins/micromega/persistent_cache.ml | 16 ++++------------ 1 file changed, 4 insertions(+), 12 deletions(-) (limited to 'plugins/micromega/persistent_cache.ml') diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml index cbacc48e4..87c9d1bbe 100644 --- a/plugins/micromega/persistent_cache.ml +++ b/plugins/micromega/persistent_cache.ml @@ -25,7 +25,9 @@ module type PHashtable = val open_in : string -> 'a t - (** [open_in f] rebuilds a table from the records stored in file [f] *) + (** [open_in f] rebuilds a table from the records stored in file [f]. + As marshaling is not type-safe, it migth segault. + *) val find : 'a t -> key -> 'a (** find has the specification of Hashtable.find *) @@ -42,7 +44,7 @@ module type PHashtable = val memo : string -> (key -> 'a) -> (key -> 'a) (** [memo cache f] returns a memo function for [f] using file [cache] as persistent table. - Note that the cache is just loaded when needed *) + Note that the cache will only be loaded when the function is used for the first time *) end @@ -89,16 +91,6 @@ let finally f rst = ); raise x -(** [from_file f] returns a hashtable by parsing records from file [f]. - Elements of the file are marshelled pairs of Caml structures. - (To ensure portability across platforms, closures are not allowed.) - - Raises Sys_error if the file cannot be open - Raises InvalidTableFormat if the file does not conform to the format - i.e, Marshal.from_channel fails -*) - - let read_key_elem inch = try Some (Marshal.from_channel inch) -- cgit v1.2.3