* http://helm.cs.unibo.it/
*)
-exception Key_already_in of string;;
-exception Key_not_found of string;;
+open Http_getter_types
class map dbname =
let perm = 420 in (* permission 644 in decimal notation *)
- let open_dbm () = Dbm.opendbm dbname [ Dbm.Dbm_rdwr; Dbm.Dbm_create ] perm in
+ let open_dbm () =
+ Http_getter_misc.mkdir ~parents:true (Filename.dirname dbname);
+ Dbm.opendbm dbname [ Dbm.Dbm_rdwr; Dbm.Dbm_create ] perm
+ in
object (self)
inherit ThreadSafe.threadSafe
val mutable db = open_dbm ()
+ val index_RE = Pcre.regexp "^theory:/.*/index.theory$"
(*initializer Gc.finalise Dbm.close db (* close db on GC *)*)
+ (* Backward compatibility code to map
+ theory:/path/t.theory into theory:/path/t/index.theory
+ when cic:/path/t/ exists *)
+ method private normalize_key key =
+ if Pcre.pmatch ~rex:index_RE key &&
+ (try ignore (Dbm.find db key); false with Not_found -> true)
+ then
+ (* we substitute /index.theory with .theory *)
+ String.sub key 0 (String.length key - 13) ^ ".theory"
+ else key
+
method add key value =
self#doWriter (lazy (
try
method resolve key =
self#doReader (lazy (
- try Dbm.find db key with Not_found -> raise (Key_not_found key)
+ try
+ Dbm.find db (self#normalize_key key)
+ with Not_found -> raise (Key_not_found key)
))
method iter (f: string -> string -> unit) =