X-Git-Url: http://matita.cs.unibo.it/gitweb/?p=helm.git;a=blobdiff_plain;f=helm%2Fhttp_getter%2Fhttp_getter_map.ml;fp=helm%2Fhttp_getter%2Fhttp_getter_map.ml;h=0000000000000000000000000000000000000000;hp=06699f1781a237153c489d950fc89e8ee6a8464c;hb=869549224eef6278a48c16ae27dd786376082b38;hpb=89262281b6e83bd2321150f81f1a0583645eb0c8 diff --git a/helm/http_getter/http_getter_map.ml b/helm/http_getter/http_getter_map.ml deleted file mode 100644 index 06699f178..000000000 --- a/helm/http_getter/http_getter_map.ml +++ /dev/null @@ -1,91 +0,0 @@ -(* - * Copyright (C) 2003: - * Stefano Zacchiroli - * for the HELM Team http://helm.cs.unibo.it/ - * - * This file is part of HELM, an Hypertextual, Electronic - * Library of Mathematics, developed at the Computer Science - * Department, University of Bologna, Italy. - * - * HELM is free software; you can redistribute it and/or - * modify it under the terms of the GNU General Public License - * as published by the Free Software Foundation; either version 2 - * of the License, or (at your option) any later version. - * - * HELM is distributed in the hope that it will be useful, - * but WITHOUT ANY WARRANTY; without even the implied warranty of - * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the - * GNU General Public License for more details. - * - * You should have received a copy of the GNU General Public License - * along with HELM; if not, write to the Free Software - * Foundation, Inc., 59 Temple Place - Suite 330, Boston, - * MA 02111-1307, USA. - * - * For details, see the HELM World-Wide-Web page, - * http://helm.cs.unibo.it/ - *) - -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 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 = - self#doWriter (lazy ( - try - Dbm.add db key value - with Dbm.Dbm_error "Entry already exists" -> raise (Key_already_in key) - )) - - method remove key = - self#doWriter (lazy ( - try - Dbm.remove db 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) - )) - - method iter (f: string -> string -> unit) = - self#doReader (lazy ( - Dbm.iter f db - )) - - method sync = - self#doWriter (lazy ( - Dbm.close db; - db <- open_dbm () - )) - - method clear = - self#doWriter (lazy ( - Dbm.close db; - List.iter - (fun ext -> - let file = dbname ^ ext in - if Sys.file_exists file then Sys.remove file) - [".dir"; ".pag"; ".db"]; - db <- open_dbm () - )) - - method close = - self#doWriter (lazy ( - Dbm.close db - )) - - end -