X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgEnvironment.ml;fp=helm%2Fsoftware%2Flambda-delta%2Fbasic_rg%2FbrgEnvironment.ml;h=0000000000000000000000000000000000000000;hb=c87a73806365feadc23300194a42ab8edb0f8b1b;hp=fb4243c74f024bb979dd2b1a941ecbdc396d9d73;hpb=f23388dbd51574725a11b0ab5373f09838a32ab5;p=helm.git diff --git a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml b/helm/software/lambda-delta/basic_rg/brgEnvironment.ml deleted file mode 100644 index fb4243c74..000000000 --- a/helm/software/lambda-delta/basic_rg/brgEnvironment.ml +++ /dev/null @@ -1,35 +0,0 @@ -(* - ||M|| This file is part of HELM, an Hypertextual, Electronic - ||A|| Library of Mathematics, developed at the Computer Science - ||T|| Department, University of Bologna, Italy. - ||I|| - ||T|| HELM is free software; you can redistribute it and/or - ||A|| modify it under the terms of the GNU General Public License - \ / version 2 or (at your option) any later version. - \ / This software is distributed as is, NO WARRANTY. - V_______________________________________________________________ *) - -module U = NUri -module L = Log -module H = U.UriHash -module B = Brg - -exception ObjectNotFound of B.message - -let hsize = 7000 -let env = H.create hsize -let entry = ref 0 - -(* Internal functions *******************************************************) - -let error uri = raise (ObjectNotFound (L.items1 (U.string_of_uri uri))) - -(* Interface functions ******************************************************) - -let set_obj f obj = - let _, uri, b = obj in - let obj = !entry, uri, b in - incr entry; H.add env uri obj; f obj - -let get_obj f uri = - try f (H.find env uri) with Not_found -> error uri