From: Stefano Zacchiroli Date: Mon, 9 Feb 2004 09:42:15 +0000 (+0000) Subject: no longer use marshalled table for unicode macros X-Git-Tag: V_0_2_3~2 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=57603e5f5f5507c21ec7cb823e5bef708441b0d0;p=helm.git no longer use marshalled table for unicode macros --- diff --git a/helm/ocaml/cic_disambiguation/.cvsignore b/helm/ocaml/cic_disambiguation/.cvsignore index b94ae04d1..93ed7a89c 100644 --- a/helm/ocaml/cic_disambiguation/.cvsignore +++ b/helm/ocaml/cic_disambiguation/.cvsignore @@ -1,7 +1,5 @@ -*.cma -*.cmo -*.cmi -*.cmx -*.cmxa +*.cm[aiox] *.cmxa *.[ao] test_lexer test_parser +macro_table.ml +make_table diff --git a/helm/ocaml/cic_disambiguation/.depend b/helm/ocaml/cic_disambiguation/.depend index b34b115f4..2a5719e54 100644 --- a/helm/ocaml/cic_disambiguation/.depend +++ b/helm/ocaml/cic_disambiguation/.depend @@ -5,10 +5,12 @@ disambiguateTypes.cmo: disambiguateTypes.cmi disambiguateTypes.cmx: disambiguateTypes.cmi disambiguateChoices.cmo: disambiguateTypes.cmi disambiguateChoices.cmi disambiguateChoices.cmx: disambiguateTypes.cmx disambiguateChoices.cmi -macro.cmo: macro.cmi -macro.cmx: macro.cmi -cicTextualLexer2.cmo: macro.cmi cicTextualLexer2.cmi -cicTextualLexer2.cmx: macro.cmx cicTextualLexer2.cmi +macro_table.cmo: macro_table.cmi +macro_table.cmx: macro_table.cmi +cicTextualParser2Macro.cmo: macro_table.cmi cicTextualParser2Macro.cmi +cicTextualParser2Macro.cmx: macro_table.cmx cicTextualParser2Macro.cmi +cicTextualLexer2.cmo: cicTextualParser2Macro.cmi cicTextualLexer2.cmi +cicTextualLexer2.cmx: cicTextualParser2Macro.cmx cicTextualLexer2.cmi cicTextualParser2.cmo: cicTextualLexer2.cmi disambiguateChoices.cmi \ disambiguateTypes.cmi cicTextualParser2.cmi cicTextualParser2.cmx: cicTextualLexer2.cmx disambiguateChoices.cmx \ diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile index ec24a4f4d..ef4ff8cc2 100644 --- a/helm/ocaml/cic_disambiguation/Makefile +++ b/helm/ocaml/cic_disambiguation/Makefile @@ -7,7 +7,8 @@ NOTATIONS = logic arit tex INTERFACE_FILES = \ disambiguateTypes.mli \ disambiguateChoices.mli \ - macro.mli \ + macro_table.mli \ + cicTextualParser2Macro.mli \ cicTextualLexer2.mli \ cicTextualParser2.mli \ disambiguate.mli @@ -18,18 +19,22 @@ IMPLEMENTATION_FILES = \ ULEXDIR := $(shell ocamlfind query ulex) LEXER_P4_OPTS = -I $(ULEXDIR) pa_ulex.cma -PARSER_P4_OPTS = pa_extend.cmo ./macro.cmo ./pa_unicode_macro.cmo +PARSER_P4_OPTS = \ + pa_extend.cmo \ + ./macro_table.cmo \ + ./cicTextualParser2Macro.cmo \ + ./pa_unicode_macro.cmo PA_P4_OPTS = q_MLast.cmo pa_extend.cmo all: cicTextualLexer2.cmo: cicTextualLexer2.ml $(OCAMLC) -pp "camlp4o $(LEXER_P4_OPTS)" -c $< -cicTextualParser2.cmo: cicTextualParser2.ml macro.cmo pa_unicode_macro.cmo +cicTextualParser2.cmo: cicTextualParser2.ml cicTextualParser2Macro.cmo pa_unicode_macro.cmo $(OCAMLC) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< cicTextualLexer2.cmx: cicTextualLexer2.ml $(OCAMLOPT) -pp "camlp4o $(LEXER_P4_OPTS)" -c $< -cicTextualParser2.cmx: cicTextualParser2.ml macro.cmo pa_unicode_macro.cmo +cicTextualParser2.cmx: cicTextualParser2.ml cicTextualParser2Macro.cmo pa_unicode_macro.cmo $(OCAMLOPT) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< %_notation.cmo: %_notation.ml cicTextualParser2.cmo @@ -37,9 +42,9 @@ cicTextualParser2.cmx: cicTextualParser2.ml macro.cmo pa_unicode_macro.cmo %_notation.cmx: %_notation.ml cicTextualParser2.cmx $(OCAMLOPT) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< -pa_unicode_macro.cmo: pa_unicode_macro.ml macro.cmo +pa_unicode_macro.cmo: pa_unicode_macro.ml cicTextualParser2Macro.cmo $(OCAMLC) -pp "camlp4o $(PA_P4_OPTS)" -c $< -pa_unicode_macro.cmx: pa_unicode_macro.ml macro.cmx +pa_unicode_macro.cmx: pa_unicode_macro.ml cicTextualParser2Macro.cmx $(OCAMLOPT) -pp "camlp4o $(PA_P4_OPTS)" -c $< LOCAL_LINKOPTS = -linkpkg $(PACKAGE).cma @@ -49,11 +54,12 @@ test_lexer: test_lexer.ml $(PACKAGE).cma test_parser: test_parser.ml $(PACKAGE).cma $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< make_table: make_table.ml - $(OCAMLC) -linkpkg -o $@ $< + $(OCAMLFIND) ocamlc -package pxp -linkpkg -o $@ $^ -.PHONY: macro_table.dump -macro_table.dump: make_table +macro_table.ml: make_table ./make_table $@ +macro_table.cmo: macro_table.ml + $(OCAMLFIND) ocamlc -c $< clean: extra_clean distclean: extra_clean @@ -64,7 +70,7 @@ extra_clean: include ../Makefile.common .PHONY: depend -depend: macro.cmi macro.cmo pa_unicode_macro.cmi pa_unicode_macro.cmo +depend: cicTextualParser2Macro.cmi cicTextualParser2Macro.cmo pa_unicode_macro.cmi pa_unicode_macro.cmo $(OCAMLDEP) -pp "camlp4o $(PARSER_P4_OPTS) $(LEXER_P4_OPTS)" $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend disambiguateTypes.cmi: disambiguateTypes.mli diff --git a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml index bcc8fda28..be2a034ac 100644 --- a/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml +++ b/helm/ocaml/cic_disambiguation/cicTextualLexer2.ml @@ -111,8 +111,8 @@ let rec token = lexer Ulexing.utf8_sub_lexeme lexbuf 1 (Ulexing.lexeme_length lexbuf - 1) in (try - return lexbuf ("SYMBOL", Macro.expand macro) - with Macro.Macro_not_found _ -> + return lexbuf ("SYMBOL", CicTextualParser2Macro.expand macro) + with CicTextualParser2Macro.Macro_not_found _ -> return lexbuf ("SYMBOL", Ulexing.utf8_lexeme lexbuf)) | eof -> return lexbuf ("EOI", "") | _ -> error lexbuf "Invalid character" diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Macro.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2Macro.ml new file mode 100644 index 000000000..972f50501 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2Macro.ml @@ -0,0 +1,33 @@ +(* Copyright (C) 2004, HELM Team. + * + * 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 Macro_not_found of string +exception Utf8_not_found of string + +let expand macro = + try + Hashtbl.find Macro_table.macro2utf8 macro + with Not_found -> raise (Macro_not_found macro) + diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2Macro.mli b/helm/ocaml/cic_disambiguation/cicTextualParser2Macro.mli new file mode 100644 index 000000000..bf3fc16b4 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/cicTextualParser2Macro.mli @@ -0,0 +1,32 @@ +(* Copyright (C) 2004, HELM Team. + * + * 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 Macro_not_found of string +exception Utf8_not_found of string + + (* @param macro name + @return utf8 string *) +val expand: string -> string + diff --git a/helm/ocaml/cic_disambiguation/macro.ml b/helm/ocaml/cic_disambiguation/macro.ml deleted file mode 100644 index a3e3cbf25..000000000 --- a/helm/ocaml/cic_disambiguation/macro.ml +++ /dev/null @@ -1,52 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * 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 Macro_not_found of string -exception Utf8_not_found of string - -let dump_file = "macro_table.dump" - -let init () = - let ic = open_in dump_file in - let (macro2utf8, utf82macro): - ((string, string) Hashtbl.t * (string, string) Hashtbl.t) - = - Marshal.from_channel ic - in - close_in ic; - (macro2utf8, utf82macro) - -let (macro2utf8, utf82macro) = init () - -let expand macro = - try - Hashtbl.find macro2utf8 macro - with Not_found -> raise (Macro_not_found macro) - -let contract utf8 = - try - Hashtbl.find utf82macro utf8 - with Not_found -> raise (Utf8_not_found utf8) - diff --git a/helm/ocaml/cic_disambiguation/macro.mli b/helm/ocaml/cic_disambiguation/macro.mli deleted file mode 100644 index 39613d0df..000000000 --- a/helm/ocaml/cic_disambiguation/macro.mli +++ /dev/null @@ -1,34 +0,0 @@ -(* Copyright (C) 2004, HELM Team. - * - * 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 Macro_not_found of string -exception Utf8_not_found of string - - (* @param macro name - @return utf8 string *) -val expand: string -> string - -val contract: string -> string - diff --git a/helm/ocaml/cic_disambiguation/macro_table.dump b/helm/ocaml/cic_disambiguation/macro_table.dump deleted file mode 100644 index 627b86b2a..000000000 Binary files a/helm/ocaml/cic_disambiguation/macro_table.dump and /dev/null differ diff --git a/helm/ocaml/cic_disambiguation/macro_table.mli b/helm/ocaml/cic_disambiguation/macro_table.mli new file mode 100644 index 000000000..729797fd8 --- /dev/null +++ b/helm/ocaml/cic_disambiguation/macro_table.mli @@ -0,0 +1,27 @@ +(* Copyright (C) 2004, HELM Team. + * + * 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/ + *) + +val macro2utf8: (string, string) Hashtbl.t + diff --git a/helm/ocaml/cic_disambiguation/make_table.ml b/helm/ocaml/cic_disambiguation/make_table.ml index 50780759d..dc4a33535 100644 --- a/helm/ocaml/cic_disambiguation/make_table.ml +++ b/helm/ocaml/cic_disambiguation/make_table.ml @@ -27,12 +27,11 @@ open Printf open Pxp_types open Pxp_ev_parser -(* Usage: make_table *) - let debug = false let debug_print s = if debug then prerr_endline s -let tables = [ + (* source files for tables xml parsing (if unmarshall=false) *) +let xml_tables = [ (* `Entities, "/usr/share/gtkmathview/entities-table.xml"; `Dictionary, "/usr/share/editex/dictionary-tex.xml" @@ -42,13 +41,6 @@ let tables = [ `Entities, "macros/extra-entities.xml"; ] -let macro2utf8 = Hashtbl.create 2000 -let utf82macro = Hashtbl.create 2000 - -let add_macro macro utf8 = - debug_print (sprintf "Adding macro %s = '%s'" macro utf8); - Hashtbl.add macro2utf8 macro utf8; - Hashtbl.add utf82macro utf8 macro let rec find_first_tag pull_parser = match pull_parser () with @@ -88,24 +80,40 @@ let iter_dictionary_file f pull_parser = in aux () -let fill_table () = - List.iter - (fun (typ, fname) -> - let entry = `Entry_document [ `Extend_dtd_fully; `Parse_xml_decl ] in - let config = { default_config with encoding = `Enc_utf8 } in - let entity_manager = - create_entity_manager ~is_document:true config (from_file fname) - in - let pull_parser = create_pull_parser config entry entity_manager in - match typ with - | `Entities -> iter_entities_file add_macro pull_parser - | `Dictionary -> iter_dictionary_file add_macro pull_parser) - tables +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 *) + in + let fill_table () = + List.iter + (fun (typ, fname) -> + let entry = `Entry_document [ `Extend_dtd_fully; `Parse_xml_decl ] in + let config = { default_config with encoding = `Enc_utf8 } in + let entity_manager = + create_entity_manager ~is_document:true config (from_file fname) + in + let pull_parser = create_pull_parser config entry entity_manager in + match typ with + | `Entities -> iter_entities_file add_macro pull_parser + | `Dictionary -> iter_dictionary_file add_macro pull_parser) + xml_tables + in + fill_table (); + macro2utf8 let main () = let oc = open_out Sys.argv.(1) in - fill_table (); - Marshal.to_channel oc (macro2utf8, utf82macro) []; + output_string oc "(* GENERATED by make_table: DO NOT EDIT! *)\n"; + output_string oc "let macro2utf8 = Hashtbl.create 2000\n"; + let macro2utf8 = parse_from_xml () in + Hashtbl.iter + (fun macro utf8 -> + fprintf oc "let _ = Hashtbl.add macro2utf8 \"%s\" \"%s\"\n" + macro (String.escaped utf8)) + macro2utf8; close_out oc let _ = main () diff --git a/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml b/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml index b1a9153ca..4ba3541e5 100644 --- a/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml +++ b/helm/ocaml/cic_disambiguation/pa_unicode_macro.ml @@ -30,7 +30,7 @@ let loc = (0, 0) let expand_unicode_macro macro = debug_print (Printf.sprintf "Expanding macro '%s' ..." macro); - let expansion = Macro.expand macro in + let expansion = CicTextualParser2Macro.expand macro in <:expr< $str:expansion$ >> let _ =