X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Focaml%2Fcic_disambiguation%2FMakefile;h=aa87de4ff2662cc3f34d10680d7e11422dd8cbc9;hb=7e9904185ceff75884783dbf0bad506b8521b857;hp=ea516c526930d5c4144ab0ccdac8477861f1e2af;hpb=95c956c8d0020ea1202d2c2ef354e2dcef641820;p=helm.git diff --git a/helm/ocaml/cic_disambiguation/Makefile b/helm/ocaml/cic_disambiguation/Makefile index ea516c526..aa87de4ff 100644 --- a/helm/ocaml/cic_disambiguation/Makefile +++ b/helm/ocaml/cic_disambiguation/Makefile @@ -2,14 +2,13 @@ PACKAGE = cic_textual_parser2 REQUIRES = \ helm-tactics helm-logger helm-cic_unification helm-cic_transformations \ - ulex pxp camlp4.gramlib -# NOTATIONS = logic arit tex -NOTATIONS = logic arit + helm-pxp helm-utf8_macros \ + ulex +NOTATIONS = logic arit tex +# NOTATIONS = logic arit INTERFACE_FILES = \ disambiguateTypes.mli \ disambiguateChoices.mli \ - macro_table.mli \ - cicTextualParser2Macro.mli \ cicTextualLexer2.mli \ cicTextualParser2.mli \ disambiguate.mli @@ -17,62 +16,37 @@ IMPLEMENTATION_FILES = \ $(patsubst %.mli, %.ml, $(INTERFACE_FILES)) \ $(patsubst %,%_notation.ml,$(NOTATIONS)) -ULEXDIR := $(shell ocamlfind query ulex) - -LEXER_P4_OPTS = -I $(ULEXDIR) pa_ulex.cma -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 cicTextualParser2Macro.cmo pa_unicode_macro.cmo - $(OCAMLC) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< + $(OCAMLC_P4) -c $< +cicTextualParser2.cmo: cicTextualParser2.ml + $(OCAMLC_P4) -c $< cicTextualLexer2.cmx: cicTextualLexer2.ml - $(OCAMLOPT) -pp "camlp4o $(LEXER_P4_OPTS)" -c $< -cicTextualParser2.cmx: cicTextualParser2.ml cicTextualParser2Macro.cmo pa_unicode_macro.cmo - $(OCAMLOPT) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< - -%_notation.cmo: %_notation.ml cicTextualParser2.cmo - $(OCAMLC) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< -%_notation.cmx: %_notation.ml cicTextualParser2.cmx - $(OCAMLOPT) -pp "camlp4o $(PARSER_P4_OPTS)" -c $< + $(OCAMLOPT_P4) -c $< +cicTextualParser2.cmx: cicTextualParser2.ml + $(OCAMLOPT_P4) -c $< -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 cicTextualParser2Macro.cmx - $(OCAMLOPT) -pp "camlp4o $(PA_P4_OPTS)" -c $< +%_notation.cmo: %_notation.ml + $(OCAMLC_P4) -c $< +%_notation.cmx: %_notation.ml + $(OCAMLOPT_P4) -c $< -LOCAL_LINKOPTS = -linkpkg $(PACKAGE).cma +LOCAL_LINKOPTS = -package helm-cic_textual_parser2 -linkpkg test: test_lexer test_parser test_lexer: test_lexer.ml $(PACKAGE).cma $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< test_parser: test_parser.ml $(PACKAGE).cma $(OCAMLC) $(LOCAL_LINKOPTS) -o $@ $< -make_table: make_table.ml - $(OCAMLFIND) ocamlc -package pxp -linkpkg -o $@ $^ - -macro_table.ml: make_table - ./make_table $@ -macro_table.cmo: macro_table.ml - $(OCAMLFIND) ocamlc -c $< clean: extra_clean distclean: extra_clean rm -f macro_table.dump extra_clean: - rm -f test_lexer test_parser make_table + rm -f test_lexer test_parser include ../Makefile.common - -.PHONY: depend -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 +OCAMLARCHIVEOPTIONS += -linkall disambiguateTypes.cmi: disambiguateTypes.mli $(OCAMLC) -c -rectypes $<