From: Stefano Zacchiroli Date: Thu, 26 Dec 2002 15:50:06 +0000 (+0000) Subject: - reimplemented 'clear' method deleting old DBs and recreating them from X-Git-Tag: v0_3_99~117 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=34ce9fa57cd6c138454a69b1a0e6675118e3abc7;p=helm.git - reimplemented 'clear' method deleting old DBs and recreating them from scratch --- diff --git a/helm/http_getter/http_getter_map.ml b/helm/http_getter/http_getter_map.ml index 9ee876181..07c2c10b4 100644 --- a/helm/http_getter/http_getter_map.ml +++ b/helm/http_getter/http_getter_map.ml @@ -24,16 +24,22 @@ * http://cs.unibo.it/helm/. *) +let debug = true;; +let debug_print s = if debug then prerr_endline s;; + exception Key_already_in of string;; exception Key_not_found of string;; class map dbname = let perm = 420 in (* permission 644 in decimal notation *) - let db = Dbm.opendbm dbname [ Dbm.Dbm_rdwr; Dbm.Dbm_create ] perm in + let open_dbm () = Dbm.opendbm dbname [ Dbm.Dbm_rdwr; Dbm.Dbm_create ] perm in + object (self) inherit ThreadSafe.threadSafe + val mutable db = open_dbm () + initializer Gc.finalise Dbm.close db (* close db on GC *) method add key value = @@ -62,7 +68,10 @@ class map dbname = method clear = self#doWriter (lazy ( - Dbm.iter (fun k _ -> Dbm.remove db k) db + Dbm.close db; + Sys.remove (dbname ^ ".dir"); + Sys.remove (dbname ^ ".pag"); + db <- open_dbm () )) end