From: Claudio Sacerdoti Coen Date: Thu, 29 Nov 2001 18:07:10 +0000 (+0000) Subject: * .mli added where needed X-Git-Tag: mlminidom_0_2_2~47 X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=298fa826610192b1a173c81b4ebf961c1c7e6609;p=helm.git * .mli added where needed * Install and uninstall implemented * Makefile improvements --- diff --git a/helm/ocaml/.cvsignore b/helm/ocaml/.cvsignore index d69218dfc..c9325bab1 100644 --- a/helm/ocaml/.cvsignore +++ b/helm/ocaml/.cvsignore @@ -8,6 +8,7 @@ META.helm-cic_cache META.helm-xml META.helm-cic_proof_checking Makefile +Makefile.common configure config.log config.cache diff --git a/helm/ocaml/Makefile.common b/helm/ocaml/Makefile.common deleted file mode 100644 index 84a252e94..000000000 --- a/helm/ocaml/Makefile.common +++ /dev/null @@ -1,50 +0,0 @@ -# This Makefile must be included by another one defining: -# $REQUIRES -# $PREDICATES -# $DEPOBJS -# $OBJECTS -# $PACKAGE -# and put in a directory where there is a .depend file. - -BIN_DIR = /usr/local/bin -OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" -OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) -OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) -OCAMLDEP = ocamldep - -ARCHIVE = $(PACKAGE).cma -ARCHIVE_OPT = $(PACKAGE).cmxa - - -$(ARCHIVE): $(OBJECTS) - $(OCAMLC) -a -o $@ $^ - -$(ARCHIVE_OPT): $(OBJECTS:.cmo=.cmx) - $(OCAMLOPT) -a -o $@ $^ - -all: $(ARCHIVE) -opt: $(ARCHIVE_OPT) - -depend: - $(OCAMLDEP) $(DEPOBJS) > .depend - -.SUFFIXES: .ml .mli .cmo .cmi .cmx -.ml.cmo: - $(OCAMLC) -c $< -.mli.cmi: - $(OCAMLC) -c $< -.ml.cmx: - $(OCAMLOPT) -c $< - -clean: - rm -f *.cm[ioax] *.cmxa *.o - -install: - #cp - -uninstall: - #rm -f - -.PHONY: all opt depend install uninstall clean - -include .depend diff --git a/helm/ocaml/Makefile.common.in b/helm/ocaml/Makefile.common.in new file mode 100644 index 000000000..a04d1a65e --- /dev/null +++ b/helm/ocaml/Makefile.common.in @@ -0,0 +1,56 @@ +# This Makefile must be included by another one defining: +# $PACKAGE +# $REQUIRES +# $PREDICATES +# $INTERFACE_FILES +# $IMPLEMENTATION_FILES +# $EXTRA_OBJECTS_TO_INSTALL +# and put in a directory where there is a .depend file. + +OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ + +OCAMLOPTIONS = -package "$(REQUIRES)" -predicates "$(PREDICATES)" +OCAMLC = ocamlfind ocamlc $(OCAMLOPTIONS) +OCAMLOPT = ocamlfind ocamlopt $(OCAMLOPTIONS) +OCAMLDEP = ocamldep + +ARCHIVE = $(PACKAGE).cma +ARCHIVE_OPT = $(PACKAGE).cmxa +OBJECTS_TO_INSTALL = $(ARCHIVE) $(ARCHIVE_OPT) $(ARCHIVE_OPT:%.cmxa=%.a) \ + $(INTERFACE_FILES) $(INTERFACE_FILES:%.mli=%.cmi) \ + $(EXTRA_OBJECTS_TO_INSTALL) + +$(ARCHIVE): $(IMPLEMENTATION_FILES:%.ml=%.cmo) + $(OCAMLC) -a -o $@ $^ + +$(ARCHIVE_OPT): $(IMPLEMENTATION_FILES:%.ml=%.cmx) + $(OCAMLOPT) -a -o $@ $^ + +all: $(ARCHIVE) +opt: $(ARCHIVE_OPT) + +depend: + $(OCAMLDEP) $(INTERFACE_FILES) $(IMPLEMENTATION_FILES) > .depend + +.SUFFIXES: .ml .mli .cmo .cmi .cmx +.ml.cmo: + $(OCAMLC) -c $< +.mli.cmi: + $(OCAMLC) -c $< +.ml.cmx: + $(OCAMLOPT) -c $< + +clean: + rm -f *.cm[ioax] *.cmxa *.o *.a + +install: + mkdir $(OCAMLFIND_DEST_DIR)/$(PACKAGE) + cp $(OBJECTS_TO_INSTALL) $(OCAMLFIND_DEST_DIR)/$(PACKAGE) + +uninstall: + cd $(OCAMLFIND_DEST_DIR)/$(PACKAGE) && rm -f $(OBJECTS_TO_INSTALL) + rmdir $(OCAMLFIND_DEST_DIR)/$(PACKAGE) + +.PHONY: all opt depend install uninstall clean + +include .depend diff --git a/helm/ocaml/Makefile.in b/helm/ocaml/Makefile.in index 83b28f78c..e5d051620 100644 --- a/helm/ocaml/Makefile.in +++ b/helm/ocaml/Makefile.in @@ -2,6 +2,9 @@ MODULES = xml urimanager getter pxp cic cic_annotations cic_annotations_cache \ cic_cache cic_proof_checking +OCAMLFIND_DEST_DIR = @OCAMLFIND_DEST_DIR@ +OCAMLFIND_META_DIR = @OCAMLFIND_META_DIR@ + METAS = $(MODULES:%=META.helm-%) CWD=`pwd` @@ -14,19 +17,23 @@ clean: $(MODULES:%=%.clean) rm -f $(METAS) dist-clean: clean - rm -f Makefile configure config.log config.cache config.status + rm -f Makefile Makefile.common configure config.log config.cache config.status $(MODULES:%=%.all): - export OCAMLPATH=$(CWD):$$OCAMLPATH ; cd $(@:%.all=%) ; make all + export OCAMLPATH=$(CWD):$$OCAMLPATH ; cd $(@:%.all=%) && make all $(MODULES:%=%.opt): - export OCAMLPATH=$(CWD):$$OCAMLPATH ; cd $(@:%.opt=%) ; make opt + export OCAMLPATH=$(CWD):$$OCAMLPATH ; cd $(@:%.opt=%) && make opt $(MODULES:%=%.depend): - export OCAMLPATH=$(CWD):$$OCAMLPATH ; cd $(@:%.depend=%) ; make depend + export OCAMLPATH=$(CWD):$$OCAMLPATH ; cd $(@:%.depend=%) && make depend $(MODULES:%=%.install): - cd $(@:%.install=%) ; make install + cd $(@:%.install=%) && make install + export TARGET=$(OCAMLFIND_META_DIR)/$(@:%.install=META.helm-%) ; \ + cp $(@:%.install=META.helm-%.src) $$TARGET && \ + echo "directory=\"$(OCAMLFIND_DEST_DIR)/$(@:%.install=%)\"" >> $$TARGET $(MODULES:%=%.uninstall): - cd $(@:%.uninstall=%) ; make uninstall + cd $(@:%.uninstall=%) && make uninstall + rm -f $(OCAMLFIND_META_DIR)/$(@:%.uninstall=META.helm-%) $(MODULES:%=%.clean): - cd $(@:%.clean=%) ; make clean + cd $(@:%.clean=%) && make clean META.helm-%: META.helm-%.src - cp $< $@ ; echo "directory=\"$(CWD)/$(@:META.helm-%=%)\"" >> $@ + cp $< $@ && echo "directory=\"$(CWD)/$(@:META.helm-%=%)\"" >> $@ diff --git a/helm/ocaml/cic/.depend b/helm/ocaml/cic/.depend index 99591c9d0..b5cfa7d59 100644 --- a/helm/ocaml/cic/.depend +++ b/helm/ocaml/cic/.depend @@ -1,11 +1,12 @@ -deannotate.cmo: cic.cmo -deannotate.cmx: cic.cmx +deannotate.cmi: cic.cmo cicParser3.cmi: cic.cmo +cicParser2.cmi: cic.cmo cicParser3.cmi +cicParser.cmi: cic.cmo +deannotate.cmo: cic.cmo deannotate.cmi +deannotate.cmx: cic.cmx deannotate.cmi cicParser3.cmo: cic.cmo cicParser3.cmi cicParser3.cmx: cic.cmx cicParser3.cmi -cicParser2.cmi: cic.cmo cicParser3.cmi cicParser2.cmo: cic.cmo cicParser3.cmi cicParser2.cmi cicParser2.cmx: cic.cmx cicParser3.cmx cicParser2.cmi -cicParser.cmi: cic.cmo cicParser.cmo: cicParser2.cmi cicParser3.cmi cicParser.cmi cicParser.cmx: cicParser2.cmx cicParser3.cmx cicParser.cmi diff --git a/helm/ocaml/cic/Makefile b/helm/ocaml/cic/Makefile index fd810f3f7..8847e49b3 100644 --- a/helm/ocaml/cic/Makefile +++ b/helm/ocaml/cic/Makefile @@ -2,9 +2,8 @@ PACKAGE = cic REQUIRES = helm-urimanager helm-pxp PREDICATES = -DEPOBJS = cic.ml deannotate.mli deannotate.ml cicParser3.mli cicParser3.ml \ - cicParser2.mli cicParser2.ml cicParser.mli cicParser.ml - -OBJECTS = cic.cmo deannotate.cmo cicParser3.cmo cicParser2.cmo cicParser.cmo +INTERFACE_FILES = deannotate.mli cicParser3.mli cicParser2.mli cicParser.mli +IMPLEMENTATION_FILES = cic.ml $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = cic.ml cic.cmi include ../Makefile.common diff --git a/helm/ocaml/cic/cic.ml b/helm/ocaml/cic/cic.ml index 8c08b0075..5c42f9e76 100644 --- a/helm/ocaml/cic/cic.ml +++ b/helm/ocaml/cic/cic.ml @@ -28,7 +28,7 @@ (* PROJECT HELM *) (* *) (* Claudio Sacerdoti Coen *) -(* 14/06/2000 *) +(* 29/11/2000 *) (* *) (* This module defines the internal representation of the objects (variables, *) (* blocks of (co)inductive definitions and constants) and the terms of cic *) diff --git a/helm/ocaml/cic/deannotate.mli b/helm/ocaml/cic/deannotate.mli new file mode 100644 index 000000000..d1bd72c07 --- /dev/null +++ b/helm/ocaml/cic/deannotate.mli @@ -0,0 +1,39 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 29/11/2000 *) +(* *) +(******************************************************************************) + +(* Useful only for fix_params *) +val expect_possible_parameters : bool ref + +val deannotate_term : Cic.annterm -> Cic.term +val deannotate_obj : Cic.annobj -> Cic.obj diff --git a/helm/ocaml/cic_annotations/.depend b/helm/ocaml/cic_annotations/.depend index ac3b26ba0..267924e89 100644 --- a/helm/ocaml/cic_annotations/.depend +++ b/helm/ocaml/cic_annotations/.depend @@ -1,2 +1,10 @@ -cicAnnotationParser.cmo: cicAnnotationParser2.cmo -cicAnnotationParser.cmx: cicAnnotationParser2.cmx +cicAnnotation2Xml.cmo: cicAnnotation2Xml.cmi +cicAnnotation2Xml.cmx: cicAnnotation2Xml.cmi +cicAnnotationHinter.cmo: cicAnnotationHinter.cmi +cicAnnotationHinter.cmx: cicAnnotationHinter.cmi +cicAnnotationParser2.cmo: cicAnnotationParser2.cmi +cicAnnotationParser2.cmx: cicAnnotationParser2.cmi +cicAnnotationParser.cmo: cicAnnotationParser2.cmi cicAnnotationParser.cmi +cicAnnotationParser.cmx: cicAnnotationParser2.cmx cicAnnotationParser.cmi +cicXPath.cmo: cicXPath.cmi +cicXPath.cmx: cicXPath.cmi diff --git a/helm/ocaml/cic_annotations/Makefile b/helm/ocaml/cic_annotations/Makefile index 738a265ec..1b85d96bc 100644 --- a/helm/ocaml/cic_annotations/Makefile +++ b/helm/ocaml/cic_annotations/Makefile @@ -2,10 +2,9 @@ PACKAGE = cic_annotations REQUIRES = helm-cic helm-xml lablgtk PREDICATES = -DEPOBJS = cicAnnotation2Xml.ml cicAnnotationHinter.ml cicAnnotationParser2.ml \ - cicAnnotationParser.ml cicXPath.ml - -OBJECTS = cicAnnotation2Xml.cmo cicAnnotationHinter.cmo \ - cicAnnotationParser2.cmo cicAnnotationParser.cmo cicXPath.cmo +INTERFACE_FILES = cicAnnotation2Xml.mli cicAnnotationHinter.mli \ + cicAnnotationParser2.mli cicAnnotationParser.mli cicXPath.mli +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = include ../Makefile.common diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml index c5410b080..5a8adfaff 100644 --- a/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml +++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.ml @@ -25,9 +25,7 @@ (*CSC codice cut & paste da cicPp e xmlcommand *) -exception ImpossiblePossible;; exception NotImplemented;; -exception BinderNotSpecified;; let dtdname = "http://www.cs.unibo.it/helm/dtd/annotations.dtd";; diff --git a/helm/ocaml/cic_annotations/cicAnnotation2Xml.mli b/helm/ocaml/cic_annotations/cicAnnotation2Xml.mli new file mode 100644 index 000000000..ba1b406b4 --- /dev/null +++ b/helm/ocaml/cic_annotations/cicAnnotation2Xml.mli @@ -0,0 +1,36 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 29/11/2000 *) +(* *) +(* *) +(******************************************************************************) + +val pp_annotation : Cic.annobj -> UriManager.uri -> Xml.token Stream.t diff --git a/helm/ocaml/cic_annotations/cicAnnotationHinter.mli b/helm/ocaml/cic_annotations/cicAnnotationHinter.mli new file mode 100644 index 000000000..6846273b3 --- /dev/null +++ b/helm/ocaml/cic_annotations/cicAnnotationHinter.mli @@ -0,0 +1,46 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 29/11/2000 *) +(* *) +(* *) +(******************************************************************************) + +val create_hints : + < annotation : GEdit.text; + annotation_hints : < children : < as_widget : 'a Gtk.obj; .. > list; + connect : < clicked : (unit -> unit) -> GtkSignal.id; + .. >; + misc : < disconnect : GtkSignal.id -> 'b; + hide : unit -> 'c; show : unit -> 'd; .. >; + .. > + array; + .. > -> + 'e * (string, Cic.anntarget) Hashtbl.t -> string -> unit diff --git a/helm/ocaml/cic_annotations/cicAnnotationParser.mli b/helm/ocaml/cic_annotations/cicAnnotationParser.mli new file mode 100644 index 000000000..473d05fe5 --- /dev/null +++ b/helm/ocaml/cic_annotations/cicAnnotationParser.mli @@ -0,0 +1,36 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 29/11/2000 *) +(* *) +(* *) +(******************************************************************************) + +val annotate : string -> (string, Cic.anntarget) Hashtbl.t -> unit diff --git a/helm/ocaml/cic_annotations/cicAnnotationParser2.mli b/helm/ocaml/cic_annotations/cicAnnotationParser2.mli new file mode 100644 index 000000000..80bc0f6b1 --- /dev/null +++ b/helm/ocaml/cic_annotations/cicAnnotationParser2.mli @@ -0,0 +1,51 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 29/11/2000 *) +(* *) +(* *) +(******************************************************************************) + +exception IllFormedXml of int +val annotate : + (string, Cic.anntarget) Hashtbl.t -> + < node_type : Pxp_document.node_type; + sub_nodes : < attribute : string -> Pxp_types.att_value; + node_type : Pxp_document.node_type; + sub_nodes : (< attribute : string -> Pxp_types.att_value; + attribute_names : string list; + data : string; + node_type : Pxp_document.node_type; + sub_nodes : 'a list; .. > as 'a) + list; + .. > + list; + .. > -> + unit diff --git a/helm/ocaml/cic_annotations/cicXPath.mli b/helm/ocaml/cic_annotations/cicXPath.mli new file mode 100644 index 000000000..5ca9a2cf6 --- /dev/null +++ b/helm/ocaml/cic_annotations/cicXPath.mli @@ -0,0 +1,37 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 29/11/2000 *) +(* *) +(* *) +(******************************************************************************) + +val get_annotation : + 'a * (string, Cic.anntarget) Hashtbl.t -> string -> string option ref diff --git a/helm/ocaml/cic_annotations_cache/Makefile b/helm/ocaml/cic_annotations_cache/Makefile index 887553062..5daa8160b 100644 --- a/helm/ocaml/cic_annotations_cache/Makefile +++ b/helm/ocaml/cic_annotations_cache/Makefile @@ -2,8 +2,8 @@ PACKAGE = cic_annotations_cache REQUIRES = helm-cic_annotations PREDICATES = -DEPOBJS = cicCache.mli cicCache.ml - -OBJECTS = cicCache.cmo +INTERFACE_FILES = cicCache.mli +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = include ../Makefile.common diff --git a/helm/ocaml/cic_cache/Makefile b/helm/ocaml/cic_cache/Makefile index 76cba058e..342124a7b 100644 --- a/helm/ocaml/cic_cache/Makefile +++ b/helm/ocaml/cic_cache/Makefile @@ -2,8 +2,8 @@ PACKAGE = cic_cache REQUIRES = helm-cic PREDICATES = -DEPOBJS = cicCache.mli cicCache.ml - -OBJECTS = cicCache.cmo +INTERFACE_FILES = cicCache.mli +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = include ../Makefile.common diff --git a/helm/ocaml/cic_proof_checking/.depend b/helm/ocaml/cic_proof_checking/.depend index da66c1502..81126bbdf 100644 --- a/helm/ocaml/cic_proof_checking/.depend +++ b/helm/ocaml/cic_proof_checking/.depend @@ -1,9 +1,11 @@ -cicPp.cmo: cicEnvironment.cmi cicPp.cmi -cicPp.cmx: cicEnvironment.cmx cicPp.cmi -cicEnvironment.cmo: cicSubstitution.cmi cicEnvironment.cmi -cicEnvironment.cmx: cicSubstitution.cmx cicEnvironment.cmi cicSubstitution.cmo: cicSubstitution.cmi cicSubstitution.cmx: cicSubstitution.cmi +cicEnvironment.cmo: cicSubstitution.cmi cicEnvironment.cmi +cicEnvironment.cmx: cicSubstitution.cmx cicEnvironment.cmi +cicPp.cmo: cicEnvironment.cmi cicPp.cmi +cicPp.cmx: cicEnvironment.cmx cicPp.cmi +cicMiniReduction.cmo: cicSubstitution.cmi cicMiniReduction.cmi +cicMiniReduction.cmx: cicSubstitution.cmx cicMiniReduction.cmi cicReduction.cmo: cicEnvironment.cmi cicPp.cmi cicSubstitution.cmi \ cicReduction.cmi cicReduction.cmx: cicEnvironment.cmx cicPp.cmx cicSubstitution.cmx \ @@ -14,5 +16,3 @@ cicTypeChecker.cmx: cicEnvironment.cmx cicPp.cmx cicReduction.cmx \ cicSubstitution.cmx cicTypeChecker.cmi cicCooking.cmo: cicEnvironment.cmi cicCooking.cmi cicCooking.cmx: cicEnvironment.cmx cicCooking.cmi -cicMiniReduction.cmo: cicSubstitution.cmi cicMiniReduction.cmi -cicMiniReduction.cmx: cicSubstitution.cmx cicMiniReduction.cmi diff --git a/helm/ocaml/cic_proof_checking/Makefile b/helm/ocaml/cic_proof_checking/Makefile index 97bd462b5..ad31350c2 100644 --- a/helm/ocaml/cic_proof_checking/Makefile +++ b/helm/ocaml/cic_proof_checking/Makefile @@ -2,13 +2,15 @@ PACKAGE = cic_proof_checking REQUIRES = helm-cic PREDICATES = -DEPOBJS = cicPp.mli cicPp.ml cicEnvironment.mli cicEnvironment.ml \ - cicSubstitution.mli cicSubstitution.ml cicReduction.mli \ - cicReduction.ml cicTypeChecker.mli cicTypeChecker.ml \ - cicCooking.mli cicCooking.ml cicMinireduction.mli cicMiniReduction.ml - -OBJECTS = cicSubstitution.cmo cicEnvironment.cmo cicPp.cmo \ - cicMiniReduction.cmo cicReduction.cmo cicTypeChecker.cmo \ - cicCooking.cmo +INTERFACE_FILES = cicSubstitution.mli cicEnvironment.mli cicPp.mli \ + cicMiniReduction.mli cicReduction.mli cicTypeChecker.mli \ + cicCooking.mli +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) + +# Metadata tools only need zeta-reduction +EXTRA_OBJECTS_TO_INSTALL = \ + cicSubstitution.cmo cicSubstitution.cmx cicSubstitution.o \ + cicMiniReduction.cmo cicMiniReduction.cmx cicMiniReduction.o + include ../Makefile.common diff --git a/helm/ocaml/configure.in b/helm/ocaml/configure.in index 715a9d105..d586e335c 100644 --- a/helm/ocaml/configure.in +++ b/helm/ocaml/configure.in @@ -1,4 +1,4 @@ -AC_INIT(Makefile.common) +AC_INIT(Makefile.in) AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no) if test $HAVE_OCAMLC = "no"; then @@ -10,6 +10,18 @@ if test $HAVE_OCAMLFIND = "no"; then AC_MSG_ERROR(could not find ocamlfind in PATH, please make sure findlib is installed) fi +AC_MSG_CHECKING("where to install the library") +OCAMLFIND_DEST_DIR="/public/sacerdot/prova" +AC_MSG_RESULT($OCAMLFIND_DEST_DIR) + +AC_MSG_CHECKING("where to install the META files") +OCAMLFIND_META_DIR="/public/sacerdot/prova/META" +AC_MSG_RESULT($OCAMLFIND_META_DIR) + +AC_SUBST(OCAMLFIND_DEST_DIR) +AC_SUBST(OCAMLFIND_META_DIR) + AC_OUTPUT([ Makefile + Makefile.common ]) diff --git a/helm/ocaml/getter/.depend b/helm/ocaml/getter/.depend index 1b3156776..2013e9b3e 100644 --- a/helm/ocaml/getter/.depend +++ b/helm/ocaml/getter/.depend @@ -1,4 +1,6 @@ -clientHTTP.cmo: configuration.cmo clientHTTP.cmi +configuration.cmo: configuration.cmi +configuration.cmx: configuration.cmi +clientHTTP.cmo: configuration.cmi clientHTTP.cmi clientHTTP.cmx: configuration.cmx clientHTTP.cmi -getter.cmo: clientHTTP.cmi configuration.cmo getter.cmi +getter.cmo: clientHTTP.cmi configuration.cmi getter.cmi getter.cmx: clientHTTP.cmx configuration.cmx getter.cmi diff --git a/helm/ocaml/getter/Makefile b/helm/ocaml/getter/Makefile index a3b941b0f..32812a747 100644 --- a/helm/ocaml/getter/Makefile +++ b/helm/ocaml/getter/Makefile @@ -2,8 +2,8 @@ PACKAGE = getter REQUIRES = pxp netclient helm-urimanager PREDICATES = -DEPOBJS = clientHTTP.mli clientHTTP.ml getter.mli getter.ml configuration.ml - -OBJECTS = configuration.cmo clientHTTP.cmo getter.cmo +INTERFACE_FILES = configuration.mli clientHTTP.mli getter.mli +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = include ../Makefile.common diff --git a/helm/ocaml/getter/configuration.mli b/helm/ocaml/getter/configuration.mli new file mode 100644 index 000000000..4d0bfbc01 --- /dev/null +++ b/helm/ocaml/getter/configuration.mli @@ -0,0 +1,48 @@ +(* Copyright (C) 2000, 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://cs.unibo.it/helm/. + *) + +(******************************************************************************) +(* *) +(* PROJECT HELM *) +(* *) +(* Claudio Sacerdoti Coen *) +(* 29/11/2000 *) +(* *) +(* *) +(******************************************************************************) + +val helm_dir : string +val dtd_dir : string +val style_dir : string +val servers_file : string +val uris_dbm : string +val dest : string +val indexname : string +val tmp_dir : string +val helm_dir : string +val getter_url : string +val processor_url : string +val annotations_dir : string +val annotations_url : string diff --git a/helm/ocaml/pxp/.depend b/helm/ocaml/pxp/.depend index 5ad7c60e2..529d934c7 100644 --- a/helm/ocaml/pxp/.depend +++ b/helm/ocaml/pxp/.depend @@ -1,2 +1,5 @@ -pxpUriResolver.cmo: csc_pxp_reader.cmo -pxpUriResolver.cmx: csc_pxp_reader.cmx +pxpUriResolver.cmi: csc_pxp_reader.cmi +csc_pxp_reader.cmo: csc_pxp_reader.cmi +csc_pxp_reader.cmx: csc_pxp_reader.cmi +pxpUriResolver.cmo: csc_pxp_reader.cmi pxpUriResolver.cmi +pxpUriResolver.cmx: csc_pxp_reader.cmx pxpUriResolver.cmi diff --git a/helm/ocaml/pxp/Makefile b/helm/ocaml/pxp/Makefile index 2a89a95f0..1ccb4244b 100644 --- a/helm/ocaml/pxp/Makefile +++ b/helm/ocaml/pxp/Makefile @@ -2,8 +2,8 @@ PACKAGE = pxp REQUIRES = helm-getter PREDICATES = -DEPOBJS = csc_pxp_reader.ml pxpUriResolver.ml - -OBJECTS = csc_pxp_reader.cmo pxpUriResolver.cmo +INTERFACE_FILES = csc_pxp_reader.mli pxpUriResolver.mli +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = include ../Makefile.common diff --git a/helm/ocaml/pxp/csc_pxp_reader.mli b/helm/ocaml/pxp/csc_pxp_reader.mli new file mode 100644 index 000000000..2d103b371 --- /dev/null +++ b/helm/ocaml/pxp/csc_pxp_reader.mli @@ -0,0 +1,46 @@ +exception Not_competent +exception Not_resolvable of exn +class type resolver = + object + method change_encoding : string -> unit + method clone : resolver + method close_all : unit + method close_in : unit + method init_rep_encoding : Pxp_types.rep_encoding -> unit + method init_warner : Pxp_types.collect_warnings -> unit + method open_in : Pxp_types.ext_id -> Lexing.lexbuf + method rep_encoding : Pxp_types.rep_encoding + end +class resolve_read_url_channel : + ?base_url:Neturl.url -> + ?close:(in_channel -> unit) -> + url_of_id:(Pxp_types.ext_id -> Neturl.url) -> + channel_of_url:(Pxp_types.ext_id -> + Neturl.url -> in_channel * Pxp_types.encoding option) -> + unit -> resolver +type spec = [ `Not_recognized | `Allowed | `Required] +val make_file_url : + ?system_encoding:Netconversion.encoding -> + ?enc:Netconversion.encoding -> string -> Neturl.url +type combination_mode = Public_before_system | System_before_public +class combine : + ?prefer:resolver -> + ?mode:combination_mode -> + resolver list -> + object + val mutable active_resolver : resolver option + val mutable clones : combine list + val mutable internal_encoding : Pxp_types.rep_encoding + val mode : combination_mode + val prefered_resolver : resolver option + val resolvers : resolver list + val mutable warner : Pxp_types.drop_warnings + method change_encoding : string -> unit + method clone : combine + method close_all : unit + method close_in : unit + method init_rep_encoding : Pxp_types.rep_encoding -> unit + method init_warner : Pxp_types.collect_warnings -> unit + method open_in : Pxp_types.ext_id -> Lexing.lexbuf + method rep_encoding : Pxp_types.rep_encoding + end diff --git a/helm/ocaml/pxp/pxpUriResolver.mli b/helm/ocaml/pxp/pxpUriResolver.mli new file mode 100644 index 000000000..d2a1210aa --- /dev/null +++ b/helm/ocaml/pxp/pxpUriResolver.mli @@ -0,0 +1,4 @@ +val from_file : + ?alt:Csc_pxp_reader.resolver list -> + ?system_encoding:Netconversion.encoding -> + ?enc:Netconversion.encoding -> string -> Pxp_yacc.source diff --git a/helm/ocaml/urimanager/Makefile b/helm/ocaml/urimanager/Makefile index 2d01dee04..2f21b369e 100644 --- a/helm/ocaml/urimanager/Makefile +++ b/helm/ocaml/urimanager/Makefile @@ -2,8 +2,8 @@ PACKAGE = urimanager REQUIRES = str PREDICATES = -DEPOBJS = uriManager.mli uriManager.ml - -OBJECTS = uriManager.cmo +INTERFACE_FILES = uriManager.mli +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = include ../Makefile.common diff --git a/helm/ocaml/xml/Makefile b/helm/ocaml/xml/Makefile index f1037d90e..502cdc18a 100644 --- a/helm/ocaml/xml/Makefile +++ b/helm/ocaml/xml/Makefile @@ -2,8 +2,8 @@ PACKAGE = xml REQUIRES = PREDICATES = -DEPOBJS = xml.mli xml.ml - -OBJECTS = xml.cmo +INTERFACE_FILES = xml.mli +IMPLEMENTATION_FILES = $(INTERFACE_FILES:%.mli=%.ml) +EXTRA_OBJECTS_TO_INSTALL = include ../Makefile.common