From: Stefano Zacchiroli Date: Fri, 16 Sep 2005 11:49:07 +0000 (+0000) Subject: uses Hashtbl.replace instead of Hashtbl.add so that: X-Git-Tag: LAST_BEFORE_NEW~118 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=77f4040c3aae06baba4c9868e5126689b16527c4;p=helm.git uses Hashtbl.replace instead of Hashtbl.add so that: 1) extra-entities.xml could be used to override undesired bindings 2) only used mapping are kept in memory at run-time --- diff --git a/helm/ocaml/utf8_macros/make_table.ml b/helm/ocaml/utf8_macros/make_table.ml index cca1d13c4..377fea64a 100644 --- a/helm/ocaml/utf8_macros/make_table.ml +++ b/helm/ocaml/utf8_macros/make_table.ml @@ -37,6 +37,8 @@ let xml_tables = [ `Entities, "data/entities-table.xml"; `Dictionary, "data/dictionary-tex.xml"; `Entities, "data/extra-entities.xml"; + (** extra-entities.xml should be the last one since it is used to override + * previous mappings. Add there overrides as needed. *) ] let iter_gen record_tag name_field value_field f fname = @@ -62,8 +64,8 @@ let parse_from_xml () = let (macro2utf8, utf82macro) = (Hashtbl.create 2000, Hashtbl.create 2000) in let add_macro macro utf8 = debug_print (sprintf "Adding macro %s = '%s'" macro utf8); - Hashtbl.add macro2utf8 macro utf8; - Hashtbl.add utf82macro utf8 macro + Hashtbl.replace macro2utf8 macro utf8; + Hashtbl.replace utf82macro utf8 macro in let fill_table () = List.iter @@ -84,12 +86,12 @@ let main () = let macro2utf8, utf82macro = parse_from_xml () in Hashtbl.iter (fun macro utf8 -> - fprintf oc "let _ = Hashtbl.add macro2utf8 \"%s\" \"%s\"\n" + fprintf oc "let _ = Hashtbl.replace macro2utf8 \"%s\" \"%s\"\n" macro (String.escaped utf8)) macro2utf8; Hashtbl.iter (fun utf8 macro -> - fprintf oc "let _ = Hashtbl.add utf82macro \"%s\" \"%s\"\n" + fprintf oc "let _ = Hashtbl.replace utf82macro \"%s\" \"%s\"\n" (String.escaped utf8) macro) utf82macro; close_out oc