META.helm-xml
META.helm-cic_proof_checking
Makefile
+Makefile.common
configure
config.log
config.cache
+++ /dev/null
-# 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
--- /dev/null
+# 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
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`
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-%=%)\"" >> $@
-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
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
(* PROJECT HELM *)
(* *)
(* Claudio Sacerdoti Coen <sacerdot@cs.unibo.it> *)
-(* 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 *)
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
-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
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
(*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";;
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 29/11/2000 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+val pp_annotation : Cic.annobj -> UriManager.uri -> Xml.token Stream.t
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 29/11/2000 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+val annotate : string -> (string, Cic.anntarget) Hashtbl.t -> unit
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 29/11/2000 *)
+(* *)
+(* *)
+(******************************************************************************)
+
+val get_annotation :
+ 'a * (string, Cic.anntarget) Hashtbl.t -> string -> string option ref
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
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
-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 \
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
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
-AC_INIT(Makefile.common)
+AC_INIT(Makefile.in)
AC_CHECK_PROG(HAVE_OCAMLC, ocamlc, yes, no)
if test $HAVE_OCAMLC = "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
])
-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
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
--- /dev/null
+(* 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 <sacerdot@cs.unibo.it> *)
+(* 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
-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
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
--- /dev/null
+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
--- /dev/null
+val from_file :
+ ?alt:Csc_pxp_reader.resolver list ->
+ ?system_encoding:Netconversion.encoding ->
+ ?enc:Netconversion.encoding -> string -> Pxp_yacc.source
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
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
projects / helm.git / commitdiff