aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
-rw-r--r--.depend19
-rw-r--r--Makefile31
-rw-r--r--bin/.cvsignore1
-rw-r--r--config/Makefile.template6
-rwxr-xr-xconfigure30
5 files changed, 83 insertions, 4 deletions
diff --git a/.depend b/.depend
index b94d84539..2895a351d 100644
--- a/.depend
+++ b/.depend
@@ -1,3 +1,4 @@
+doc/syntax.cmi: parsing/ast.cmi
ide/config_parser.cmi: lib/util.cmi
ide/coq.cmi: kernel/environ.cmi pretyping/evd.cmi kernel/names.cmi \
kernel/term.cmi lib/util.cmi toplevel/vernacexpr.cmo
@@ -435,6 +436,8 @@ contrib/xml/doubleTypeInference.cmi: contrib/xml/acic.cmo kernel/environ.cmi \
pretyping/evd.cmi kernel/term.cmi
contrib/xml/xmlcommand.cmi: library/libnames.cmi
ide/utils/configwin.cmi: ide/utils/uoptions.cmi
+tools/coqdoc/output.cmi: tools/coqdoc/index.cmi
+tools/coqdoc/pretty.cmi: tools/coqdoc/index.cmi
config/coq_config.cmo: config/coq_config.cmi
config/coq_config.cmx: config/coq_config.cmi
dev/db_printers.cmo: kernel/names.cmi lib/pp.cmi
@@ -455,6 +458,8 @@ dev/top_printers.cmx: parsing/ast.cmx toplevel/cerrors.cmx proofs/clenv.cmx \
kernel/term.cmx pretyping/termops.cmx kernel/univ.cmx
doc/parse.cmo: parsing/ast.cmi
doc/parse.cmx: parsing/ast.cmx
+doc/syntax.cmo: parsing/ast.cmi contrib/interface/parse.cmo doc/syntax.cmi
+doc/syntax.cmx: parsing/ast.cmx contrib/interface/parse.cmx doc/syntax.cmi
ide/blaster_window.cmo: ide/coq.cmi ide/ideutils.cmi
ide/blaster_window.cmx: ide/coq.cmx ide/ideutils.cmx
ide/command_windows.cmo: ide/coq.cmi ide/coq_commands.cmo ide/ideutils.cmi \
@@ -3239,6 +3244,20 @@ ide/utils/okey.cmo: ide/utils/okey.cmi
ide/utils/okey.cmx: ide/utils/okey.cmi
ide/utils/uoptions.cmo: ide/utils/uoptions.cmi
ide/utils/uoptions.cmx: ide/utils/uoptions.cmi
+tools/coqdoc/alpha.cmo: tools/coqdoc/alpha.cmi
+tools/coqdoc/alpha.cmx: tools/coqdoc/alpha.cmi
+tools/coqdoc/index.cmo: tools/coqdoc/alpha.cmi tools/coqdoc/index.cmi
+tools/coqdoc/index.cmx: tools/coqdoc/alpha.cmx tools/coqdoc/index.cmi
+tools/coqdoc/main.cmo: config/coq_config.cmi tools/coqdoc/index.cmi \
+ tools/coqdoc/output.cmi tools/coqdoc/pretty.cmi
+tools/coqdoc/main.cmx: config/coq_config.cmx tools/coqdoc/index.cmx \
+ tools/coqdoc/output.cmx tools/coqdoc/pretty.cmx
+tools/coqdoc/output.cmo: tools/coqdoc/index.cmi tools/coqdoc/output.cmi
+tools/coqdoc/output.cmx: tools/coqdoc/index.cmx tools/coqdoc/output.cmi
+tools/coqdoc/pretty.cmo: tools/coqdoc/index.cmi tools/coqdoc/output.cmi \
+ tools/coqdoc/pretty.cmi
+tools/coqdoc/pretty.cmx: tools/coqdoc/index.cmx tools/coqdoc/output.cmx \
+ tools/coqdoc/pretty.cmi
tactics/tauto.cmo: parsing/grammar.cma
tactics/tauto.cmx: parsing/grammar.cma
tactics/eqdecide.cmo: parsing/grammar.cma
diff --git a/Makefile b/Makefile
index dbb6540f9..276d779a5 100644
--- a/Makefile
+++ b/Makefile
@@ -62,7 +62,8 @@ else
HIDE = @
endif
-LOCALINCLUDES=-I config -I tools -I scripts -I lib -I kernel -I library \
+LOCALINCLUDES=-I config -I tools -I tools/coqdoc \
+ -I scripts -I lib -I kernel -I library \
-I proofs -I tactics -I pretyping \
-I interp -I toplevel -I parsing -I ide/utils \
-I ide -I translate \
@@ -1045,10 +1046,12 @@ COQMAKEFILE=bin/coq_makefile$(EXE)
GALLINA=bin/gallina$(EXE)
COQTEX=bin/coq-tex$(EXE)
COQWC=bin/coqwc$(EXE)
+COQDOC=bin/coqdoc$(EXE)
COQVO2XML=bin/coq_vo2xml$(EXE)
RUNCOQVO2XML=coq_vo2xml$(EXE) # Uses the one in PATH and not the one in bin
-TOOLS=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQVO2XML) $(COQWC)
+TOOLS=$(COQDEP) $(COQMAKEFILE) $(GALLINA) $(COQTEX) $(COQVO2XML) \
+ $(COQWC) $(COQDOC)
tools:: $(TOOLS) dev/top_printers.cmo
@@ -1082,6 +1085,16 @@ $(COQWC): tools/coqwc.cmo
$(SHOW)'OCAMLC -o $@'
$(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ tools/coqwc.cmo
+beforedepend:: tools/coqdoc/pretty.ml tools/coqdoc/index.ml
+
+COQDOCCMO=$(CONFIG) tools/coqdoc/alpha.cmo tools/coqdoc/index.cmo \
+ tools/coqdoc/output.cmo tools/coqdoc/pretty.cmo \
+ tools/coqdoc/main.cmo
+
+$(COQDOC): $(COQDOCCMO)
+ $(SHOW)'OCAMLC -o $@'
+ $(HIDE)$(OCAMLC) $(BYTEFLAGS) -custom -o $@ str.cma unix.cma $(COQDOCCMO)
+
COQVO2XMLCMO=$(CONFIG) toplevel/usage.cmo tools/coq_vo2xml.cmo
$(COQVO2XML): $(COQVO2XMLCMO)
@@ -1091,6 +1104,7 @@ $(COQVO2XML): $(COQVO2XMLCMO)
clean::
rm -f tools/coqdep_lexer.ml tools/gallina_lexer.ml
rm -f tools/coqwc.ml
+ rm -f tools/coqdoc/pretty.ml tools/coqdoc/index.ml
archclean::
rm -f $(TOOLS)
@@ -1201,7 +1215,7 @@ install-allreals::
cp $$f $(FULLCOQLIB)/`dirname $$f`; \
done
-install-coq-info: install-coq-manpages install-emacs
+install-coq-info: install-coq-manpages install-emacs install-latex
MANPAGES=man/coq-tex.1 man/coqdep.1 man/gallina.1 \
man/coqc.1 man/coqtop.1 man/coqtop.byte.1 man/coqtop.opt.1 \
@@ -1215,6 +1229,17 @@ install-emacs:
$(MKDIR) $(FULLEMACSLIB)
cp tools/coq.el tools/coq-inferior.el $(FULLEMACSLIB)
+# where to put the coqdoc style file
+TEXDIR = $(BASETEXDIR)/tex/latex/misc
+
+# command to update TeX' kpathsea database
+UPDATETEX = $(MKTEXLSR) /usr/share/texmf /var/spool/texmf $(BASETEXDIR) > /dev/null
+
+install-latex:
+ $(MKDIR) $(TEXDIR)
+ cp tools/coqdoc/coqdoc.sty $(TEXDIR)
+ -$(UPDATETEX)
+
###########################################################################
# Documentation
# Literate programming (with ocamlweb)
diff --git a/bin/.cvsignore b/bin/.cvsignore
index 32c168302..e5e3c2104 100644
--- a/bin/.cvsignore
+++ b/bin/.cvsignore
@@ -17,3 +17,4 @@ coqide.opt
coqtopnew.opt
coqtopnew.byte
coqwc
+coqdoc
diff --git a/config/Makefile.template b/config/Makefile.template
index 0749c3540..d3f853f17 100644
--- a/config/Makefile.template
+++ b/config/Makefile.template
@@ -85,6 +85,12 @@ INSTALL=COQTOPDIRECTORY/bin/ARCHITECTURE/coqinstallEXECUTEEXTENSION
# the command MKDIR (try to replace it with mkdirhier if you have problems)
MKDIR=mkdir -p
+# where to put the coqdoc.sty style file
+BASETEXDIR=TEXDIRECTORY
+
+# command to update TeX' kpathsea database
+MKTEXLSR=MKTEXLSRCOMMAND
+
#the command STRIP
# Unix systems and profiling: true
# Unix systems and no profiling: strip
diff --git a/configure b/configure
index 162f0cb78..35d48ed7c 100755
--- a/configure
+++ b/configure
@@ -36,6 +36,7 @@ libdir_spec=no
mandir_spec=no
emacslib_spec=no
emacs_spec=no
+texdir_spec=no
reals_opt=no
reals=all
arch_spec=no
@@ -55,6 +56,8 @@ while : ; do
libdir=$2/lib/coq
mandir_spec=yes
mandir=$2/man
+ texdir_spec=yes
+ texdir=$2/share/texmf
shift;;
-local|--local) local=true
bindir_spec=yes
@@ -65,6 +68,8 @@ while : ; do
mandir=$COQTOP/man
emacslib_spec=yes
emacslib=$COQTOP/tools/emacs
+ texdir_spec=yes
+ texdir=$COQTOP/share/texmf
reals_opt=yes
reals=all;;
-src|--src) COQTOP=$2
@@ -84,6 +89,9 @@ while : ; do
-emacs |--emacs) emacs_spec=yes
emacs=$2
shift;;
+ -texdir|--texdir) texdir_spec=yes
+ texdir=$2
+ shift;;
-arch|--arch) arch_spec=yes
arch=$2
shift;;
@@ -151,7 +159,8 @@ case $ARCH in
bindir_def=/usr/local/bin
libdir_def=/usr/local/lib/coq
mandir_def=/usr/local/man
- emacslib_def=/usr/share/emacs/site-lisp;;
+ emacslib_def=/usr/share/emacs/site-lisp
+ texdir_def=/usr/share/texmf;;
esac
emacs_def=emacs
@@ -200,6 +209,17 @@ case $emacslib_spec in
yes) EMACSLIB=$emacslib;;
esac
+case $texdir_spec in
+ no) echo "Where should I install TeX/LaTeX files [$texdir_def] ?"
+ read TEXDIR
+
+ case $TEXDIR in
+ "") TEXDIR=$texdir_def;;
+ *) true;;
+ esac;;
+ yes) TEXDIR=$texdir;;
+esac
+
case $reals_opt in
no) echo "Should I compile the complete theory of real analysis [Y/N, default is Y] ?"
read reals_ans
@@ -357,6 +377,12 @@ case $ARCH in
fi
esac
+# mktexlsr
+MKTEXLSR=`which mktexlsr`
+case $MKTEXLSR in
+ "") MKTEXLSR=true;;
+esac
+
# Summary of the configuration
echo ""
@@ -465,6 +491,8 @@ sed -e "s|LOCALINSTALLATION|$local|" \
-e "s|MANDIRDIRECTORY|$MANDIR|" \
-e "s|EMACSLIBDIRECTORY|$EMACSLIB|" \
-e "s|EMACSCOMMAND|$EMACS|" \
+ -e "s|TEXDIRECTORY|$TEXDIR|" \
+ -e "s|MKTEXLSRCOMMAND|$MKTEXLSR|" \
-e "s|ARCHITECTURE|$ARCH|" \
-e "s|OSDEPENDENTLIBS|$OSDEPLIBS|" \
-e "s|OSDEPENDENTP4OPTFLAGS|$OSDEPP4OPTFLAGS|" \