X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;ds=sidebyside;f=helm%2Fsoftware%2Fhelena%2Fsrc%2Fbasic_rg%2FbrgEnvironment.ml;h=01a38f89ffeffa52e296b023b3816d083f0389f0;hb=2e97c767bc072f5ba238725ff1f738fc91a0135a;hp=d2daed49a26fc96820331ea5416ebf5de3082a5b;hpb=d9861cbe2be2023fe6c183747eb5d8f2b56d82ba;p=helm.git diff --git a/helm/software/helena/src/basic_rg/brgEnvironment.ml b/helm/software/helena/src/basic_rg/brgEnvironment.ml index d2daed49a..01a38f89f 100644 --- a/helm/software/helena/src/basic_rg/brgEnvironment.ml +++ b/helm/software/helena/src/basic_rg/brgEnvironment.ml @@ -9,19 +9,26 @@ \ / This software is distributed as is, NO WARRANTY. V_______________________________________________________________ *) -module U = NUri -module K = U.UriHash -module E = Entity +module U = NUri +module UH = U.UriHash +module G = Options +module E = Entity let hsize = 7000 -let env = K.create hsize +let env = UH.create hsize (* Interface functions ******************************************************) (* decps *) let set_entity entity = - let _, uri, _ = entity in - K.add env uri entity; entity +IFDEF EXPAND THEN + let ra, na, uri, b = entity in + let entity0 = if !G.expand then ra, E.node_attrs ~apix:0 (), uri, b else entity in + UH.add env uri entity0; entity +ELSE + let _, _, uri, _ = entity in + UH.add env uri entity; entity +END let get_entity uri = - try K.find env uri with Not_found -> [], uri, E.Void + try UH.find env uri with Not_found -> E.empty_root, E.empty_node, uri, E.Void