Imported Upstream snapshot 8.3~beta0+13298

1 files changed, 52 insertions, 30 deletions

diff --git a/Makefile.doc b/Makefile.doc
index f481d681..56daaa85 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -36,22 +36,20 @@ tutorial: \
 stdlib: \
   doc/stdlib/html/index.html doc/stdlib/Library.ps doc/stdlib/Library.pdf
 
-faq:\
-  doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf
+faq: doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf
 
-rectutorial:\
-  doc/RecTutorial/RecTutorial.html \
+rectutorial: doc/RecTutorial/RecTutorial.html \
   doc/RecTutorial/RecTutorial.ps doc/RecTutorial/RecTutorial.pdf
 
 ######################################################################
 ### Implicit rules
 ######################################################################
 
-ifeq ($(QUICK),1)
+ifdef QUICK
 %.v.tex: %.tex
 	(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
 else
-%.v.tex: %.tex | $(COQTEX) $(COQTOPEXE) $(CONTRIBVO) $(CONTRIBCMO) $(THEORIESVO)
+%.v.tex: %.tex $(COQTEX) $(COQTOPEXE) $(PLUGINSVO) $(THEORIESVO)
 	(cd `dirname $<`; $(COQSRC)/$(COQTEX) $(COQTEXOPTS) `basename $<`)
 endif
 
@@ -68,6 +66,9 @@ endif
 HIDEBIBTEXINFO=| grep -v "^A level-1 auxiliary file"
 SHOWMAKEINDEXERROR=egrep '^!! Input index error|^\*\* Input style error|^   --'
 
+# Empty subsection levels in faq are on purpose
+HEVEAFAQFILTER=2>&1 | grep -v "^Warning: List with no item"
+
 ######################################################################
 # Common
 ######################################################################
@@ -81,11 +82,12 @@ doc/common/version.tex: config/Makefile
 # Reference Manual
 ######################################################################
 
+
 ### Reference Manual (printable format)
 
 # The second LATEX compilation is necessary otherwise the pages of the index
 # are not correct (don't know why...) - BB
-doc/refman/Reference-Manual.dvi: $(DOCCOMMON) $(REFMANFILES) doc/refman/Reference-Manual.tex
+doc/refman/Reference-Manual.dvi: $(REFMANFILES) doc/refman/Reference-Manual.tex
 	@(cd doc/refman;\
 	$(LATEX) -interaction=batchmode Reference-Manual;\
 	$(BIBTEX) -terse Reference-Manual $(HIDEBIBTEXINFO);\
@@ -102,7 +104,7 @@ doc/refman/Reference-Manual.dvi: $(DOCCOMMON) $(REFMANFILES) doc/refman/Referenc
 	$(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\
 	../tools/show_latex_messages -no-overfull Reference-Manual.log)
 
-doc/refman/Reference-Manual.pdf: $(DOCCOMMON) $(REFMANFILES) doc/refman/Reference-Manual.tex
+doc/refman/Reference-Manual.pdf: $(REFMANFILES) doc/refman/Reference-Manual.tex
 	(cd doc/refman;\
 	$(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\
 	../tools/show_latex_messages -no-overfull Reference-Manual.log)
@@ -125,7 +127,7 @@ doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
 	$(INSTALLLIB) $(REFMANPNGFILES) doc/refman/html
 	(cd doc/refman/html; hacha -nolinks -tocbis -o toc.html ../styles.hva ../Reference-Manual.html)
 	$(INSTALLLIB) doc/refman/cover.html doc/refman/html/index.html
-	-$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html
+	$(INSTALLLIB) doc/common/styles/html/$(HTMLSTYLE)/*.css doc/refman/html
 
 refman-quick:
 	(cd doc/refman;\
@@ -169,7 +171,7 @@ doc/faq/FAQ.v.pdf: doc/common/version.tex doc/common/title.tex doc/faq/FAQ.v.dvi
 	../tools/show_latex_messages FAQ.v.log)
 
 doc/faq/FAQ.v.html: doc/faq/FAQ.v.dvi # to ensure FAQ.v.bbl
-	(cd doc/faq; $(HEVEA) $(HEVEAOPTS) FAQ.v.tex)
+	(cd doc/faq; ($(HEVEA) $(HEVEAOPTS) FAQ.v.tex $(HEVEAFAQFILTER)))
 
 doc/faq/html/index.html: doc/faq/FAQ.v.html
 	- rm -rf doc/faq/html
@@ -183,44 +185,52 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html
 
 ### Standard library (browsable html format)
 
-ifeq ($(QUICK),1)
-doc/stdlib/html/genindex.html:
+ifdef QUICK
+doc/stdlib/index-body.html:
+	- rm -rf doc/stdlib/html
+	$(MKDIR) doc/stdlib/html
+	$(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \
+	  -R theories Coq $(THEORIESVO:.vo=.v)
+	mv doc/stdlib/html/index.html doc/stdlib/index-body.html
 else
-doc/stdlib/html/genindex.html: | $(COQDOC) $(THEORIESVO)
-endif
+doc/stdlib/index-body.html: $(COQDOC) $(THEORIESVO)
 	- rm -rf doc/stdlib/html
 	$(MKDIR) doc/stdlib/html
-	$(COQDOC) -q -d doc/stdlib/html --with-header doc/common/styles/html/$(HTMLSTYLE)/header.html --with-footer doc/common/styles/html/$(HTMLSTYLE)/footer.html --multi-index --html -g \
+	$(COQDOC) -q -boot -d doc/stdlib/html --multi-index --html -g --utf8 \
 	  -R theories Coq $(THEORIESVO:.vo=.v)
-	mv doc/stdlib/html/index.html doc/stdlib/html/genindex.html
+	mv doc/stdlib/html/index.html doc/stdlib/index-body.html
+endif
 
 doc/stdlib/index-list.html: doc/stdlib/index-list.html.template doc/stdlib/make-library-index
 	./doc/stdlib/make-library-index doc/stdlib/index-list.html
 
-doc/stdlib/html/index.html: doc/stdlib/html/genindex.html doc/stdlib/index-list.html
-	cat doc/common/styles/html/$(HTMLSTYLE)/header.html doc/stdlib/index-list.html > $@
-	cat doc/common/styles/html/$(HTMLSTYLE)/footer.html >> $@
+doc/stdlib/html/index.html: doc/stdlib/index-list.html doc/stdlib/index-body.html doc/stdlib/index-trailer.html
+	cat doc/stdlib/index-list.html > $@
+	sed -n -e '/<table>/,/<\/table>/p' doc/stdlib/index-body.html >> $@
+	cat doc/stdlib/index-trailer.html >> $@
 
 ### Standard library (light version, full version is definitely too big)
 
-ifeq ($(QUICK),1)
+ifdef QUICK
 doc/stdlib/Library.coqdoc.tex:
+	$(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
+            -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@
 else
-doc/stdlib/Library.coqdoc.tex: | $(COQDOC) $(THEORIESLIGHTVO)
-endif
-	$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
+doc/stdlib/Library.coqdoc.tex: $(COQDOC) $(THEORIESLIGHTVO)
+	$(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
             -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@
+endif
 
 doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
 	(cd doc/stdlib;\
 	$(LATEX) -interaction=batchmode Library;\
 	$(LATEX) -interaction=batchmode Library > /dev/null;\
-	../tools/show_latex_messages Library.log)
+	../tools/show_latex_messages -no-overfull Library.log)
 
 doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.dvi
 	(cd doc/stdlib;\
 	$(PDFLATEX) -interaction=batchmode Library;\
-	../tools/show_latex_messages Library.log)
+	../tools/show_latex_messages -no-overfull Library.log)
 
 ######################################################################
 # Tutorial on inductive types
@@ -248,21 +258,23 @@ doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex
 
 # Not robust, improve...
 ide/index_urls.txt: doc/refman/html/index.html
-	@ rm -f ide/index_urls.txt
-	cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > ide/index_urls.txt
+	@ rm -f doc/refman/html/index_urls.txt
+	cat doc/refman/html/command-index.html doc/refman/html/tactic-index.html | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > doc/refman/html/index_urls.txt
 
 
 ######################################################################
 # Install all documentation files
 ######################################################################
 
-install-doc: install-doc-meta install-doc-html install-doc-printable
+.PHONY: install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-url
+
+install-doc: install-doc-meta install-doc-html install-doc-printable install-doc-index-url
 
 install-doc-meta:
 	$(MKDIR) $(FULLDOCDIR)
 	$(INSTALLLIB) doc/LICENSE $(FULLDOCDIR)/LICENSE.doc
 
-install-doc-html:
+install-doc-html: 
 	$(MKDIR) $(addprefix $(FULLDOCDIR)/html/, refman stdlib faq)
 	$(INSTALLLIB) doc/refman/html/* $(FULLDOCDIR)/html/refman 
 	$(INSTALLLIB) doc/stdlib/html/* $(FULLDOCDIR)/html/stdlib 
@@ -270,7 +282,7 @@ install-doc-html:
 	$(INSTALLLIB) doc/faq/html/* $(FULLDOCDIR)/html/faq
 	$(INSTALLLIB) doc/tutorial/Tutorial.v.html $(FULLDOCDIR)/html/Tutorial.html
 
-install-doc-printable:
+install-doc-printable: 
 	$(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf
 	$(INSTALLLIB) doc/refman/Reference-Manual.pdf \
 		doc/stdlib/Library.pdf $(FULLDOCDIR)/pdf
@@ -282,3 +294,13 @@ install-doc-printable:
 	$(INSTALLLIB) doc/tutorial/Tutorial.v.ps $(FULLDOCDIR)/ps/Tutorial.ps
 	$(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps
 	$(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps
+
+install-doc-index-url:
+	$(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf
+	$(INSTALLLIB) doc/refman/html/index_urls.txt \
+		$(FULLDOCDIR)/html/refman 
+
+# For emacs:
+# Local Variables:
+# mode: makefile
+# End: