X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Fbroker%2Fhbugs_broker_registry.ml;h=644f0c53f5354bef66e988f815833449f4fad5c7;hb=a4df9661e15509e5da6ed9c57e3ab6a27a440c3f;hp=adf8bc379f022c765aa932f7934dcd5a475f7eab;hpb=3c1a6c534877f7b7266809e4d92de02c7f1ee9d4;p=helm.git diff --git a/helm/hbugs/broker/hbugs_broker_registry.ml b/helm/hbugs/broker/hbugs_broker_registry.ml index adf8bc379..644f0c53f 100644 --- a/helm/hbugs/broker/hbugs_broker_registry.ml +++ b/helm/hbugs/broker/hbugs_broker_registry.ml @@ -1,5 +1,7 @@ (* - * Copyright (C) 2003, HELM Team. + * 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 @@ -21,11 +23,12 @@ * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. + * http://helm.cs.unibo.it/ *) open Hbugs_misc;; open Hbugs_types;; +open Printf;; exception Client_already_in of client_id;; exception Client_not_found of client_id;; @@ -34,27 +37,44 @@ exception Musing_not_found of musing_id;; exception Tutor_already_in of tutor_id;; exception Tutor_not_found of tutor_id;; +class type registry = + object + method dump: string + method purge: unit + end + +let expire_time = 1800. (* 30 minutes *) + class clients = object (self) inherit ThreadSafe.threadSafe + val timetable: (client_id, float) Hashtbl.t = Hashtbl.create 17 val urls: (client_id, string) Hashtbl.t = Hashtbl.create 17 val subscriptions: (client_id, tutor_id list) Hashtbl.t = Hashtbl.create 17 + (** INVARIANT: each client registered has an entry in 'urls' hash table + _and_ in 'subscriptions hash table even if it hasn't yet invoked + 'subscribe' method *) + method register id url = self#doWriter (lazy ( if Hashtbl.mem urls id then raise (Client_already_in id) else begin Hashtbl.add urls id url; - Hashtbl.add subscriptions id [] + Hashtbl.add subscriptions id []; + Hashtbl.add timetable id (Unix.time ()) end )) + method private remove id = + Hashtbl.remove urls id; + Hashtbl.remove subscriptions id; + Hashtbl.remove timetable id method unregister id = self#doWriter (lazy ( - if Hashtbl.mem urls id then begin - Hashtbl.remove urls id; - Hashtbl.remove subscriptions id - end else + if Hashtbl.mem urls id then + self#remove id + else raise (Client_not_found id) )) method isAuthenticated id = self#doReader (lazy ( @@ -79,6 +99,30 @@ class clients = raise (Client_not_found id) )) + method dump = self#doReader (lazy ( + "\n" ^ + (Hashtbl.fold + (fun id url dump -> + (dump ^ + (sprintf "\n" id url) ^ + "\n" ^ + (String.concat "\n" (* id's subscriptions *) + (List.map + (fun tutor_id -> sprintf "\n" tutor_id) + (Hashtbl.find subscriptions id))) ^ + "\n\n")) + urls "") ^ + "" + )) + method purge = self#doWriter (lazy ( + let now = Unix.time () in + Hashtbl.iter + (fun id birthday -> + if now -. birthday > expire_time then + self#remove id) + timetable + )) + end class tutors = @@ -86,18 +130,24 @@ class tutors = inherit ThreadSafe.threadSafe + val timetable: (tutor_id, float) Hashtbl.t = Hashtbl.create 17 val tbl: (tutor_id, string * hint_type * string) Hashtbl.t = Hashtbl.create 17 method register id url hint_type dsc = self#doWriter (lazy ( if Hashtbl.mem tbl id then raise (Tutor_already_in id) - else - Hashtbl.add tbl id (url, hint_type, dsc) + else begin + Hashtbl.add tbl id (url, hint_type, dsc); + Hashtbl.add timetable id (Unix.time ()) + end )) + method private remove id = + Hashtbl.remove tbl id; + Hashtbl.remove timetable id method unregister id = self#doWriter (lazy ( if Hashtbl.mem tbl id then - Hashtbl.remove tbl id + self#remove id else raise (Tutor_not_found id) )) @@ -127,6 +177,26 @@ class tutors = (fun id (url, hint_type, dsc) idx -> (id, dsc) :: idx) tbl [] )) + method dump = self#doReader (lazy ( + "\n" ^ + (Hashtbl.fold + (fun id (url, hint_type, dsc) dump -> + dump ^ + (sprintf +"\n%s\n%s\n" + id url hint_type dsc)) + tbl "") ^ + "" + )) + method purge = self#doWriter (lazy ( + let now = Unix.time () in + Hashtbl.iter + (fun id birthday -> + if now -. birthday > expire_time then + self#remove id) + timetable + )) + end class musings = @@ -134,25 +204,33 @@ class musings = inherit ThreadSafe.threadSafe + val timetable: (musing_id, float) Hashtbl.t = Hashtbl.create 17 val musings: (musing_id, client_id * tutor_id) Hashtbl.t = Hashtbl.create 17 val clients: (client_id, musing_id) Hashtbl.t = Hashtbl.create 17 val tutors: (tutor_id, musing_id) Hashtbl.t = Hashtbl.create 17 + (** INVARIANT: each registered musing has + an entry in 'musings' table, an entry in 'clients' table and an entry in + 'tutors' table *) + method register musing_id client_id tutor_id = self#doWriter (lazy ( if Hashtbl.mem musings musing_id then raise (Musing_already_in musing_id) else begin Hashtbl.add musings musing_id (client_id, tutor_id); Hashtbl.add clients client_id musing_id; - Hashtbl.add tutors tutor_id musing_id + Hashtbl.add tutors tutor_id musing_id; + Hashtbl.add timetable musing_id (Unix.time ()) end )) + method private remove id = + Hashtbl.remove musings id; + hashtbl_remove_all clients id; + hashtbl_remove_all tutors id; + Hashtbl.remove timetable id method unregister id = self#doWriter (lazy ( - if Hashtbl.mem musings id then begin - Hashtbl.remove musings id; - hashtbl_remove_all clients id; - hashtbl_remove_all tutors id - end + if Hashtbl.mem musings id then + self#remove id )) method getByMusingId id = self#doReader (lazy ( try @@ -166,5 +244,24 @@ class musings = Hashtbl.find_all tutors id )) + method dump = self#doReader (lazy ( + "\n" ^ + (Hashtbl.fold + (fun mid (cid, tid) dump -> + dump ^ + (sprintf "\n" + mid cid tid)) + musings "") ^ + "" + )) + method purge = self#doWriter (lazy ( + let now = Unix.time () in + Hashtbl.iter + (fun id birthday -> + if now -. birthday > expire_time then + self#remove id) + timetable + )) + end