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 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
- Dbm.add db key value
+ Dbm.add db (self#normalize_key key) value
with Dbm.Dbm_error "Entry already exists" -> raise (Key_already_in key)
))
method replace key value =
self#doWriter (lazy (
- Dbm.replace db key value
+ Dbm.replace db (self#normalize_key key) value
))
method remove key =
self#doWriter (lazy (
try
- Dbm.remove db key
+ Dbm.remove db (self#normalize_key key)
with Dbm.Dbm_error "dbm_delete" -> raise (Key_not_found key)
))
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) =