Imported Upstream version 8.4~betaupstream/8.4_beta

1 files changed, 75 insertions, 32 deletions

diff --git a/Makefile.doc b/Makefile.doc
index c81d779c..59eb2fe8 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -11,9 +11,12 @@
 ### General rules
 ######################################################################
 
-.PHONY: doc doc-html doc-pdf doc-ps refman tutorial stdlib faq rectutorial
+.PHONY: doc doc-html doc-pdf doc-ps refman refman-quick tutorial
+.PHONY: stdlib full-stdlib faq rectutorial
 
-doc: refman faq tutorial rectutorial stdlib ide/index_urls.txt
+INDEXURLS:=doc/refman/html/index_urls.txt
+
+doc: refman faq tutorial rectutorial stdlib $(INDEXURLS)
 
 doc-html:\
   doc/tutorial/Tutorial.v.html doc/refman/html/index.html \
@@ -36,6 +39,9 @@ tutorial: \
 stdlib: \
   doc/stdlib/html/index.html doc/stdlib/Library.ps doc/stdlib/Library.pdf
 
+full-stdlib: \
+  doc/stdlib/html/index.html doc/stdlib/FullLibrary.ps doc/stdlib/FullLibrary.pdf
+
 faq: doc/faq/html/index.html doc/faq/FAQ.v.ps doc/faq/FAQ.v.pdf
 
 rectutorial: doc/RecTutorial/RecTutorial.html \
@@ -101,7 +107,7 @@ doc/refman/Reference-Manual.dvi: $(REFMANFILES) doc/refman/Reference-Manual.tex
 	$(LATEX) -interaction=batchmode Reference-Manual > /dev/null;\
 	../tools/show_latex_messages -no-overfull Reference-Manual.log)
 
-doc/refman/Reference-Manual.pdf: $(REFMANFILES) doc/refman/Reference-Manual.tex
+doc/refman/Reference-Manual.pdf: doc/refman/Reference-Manual.dvi
 	(cd doc/refman;\
 	$(PDFLATEX) -interaction=batchmode Reference-Manual.tex;\
 	../tools/show_latex_messages -no-overfull Reference-Manual.log)
@@ -117,14 +123,17 @@ doc/refman/cover.html: doc/common/styles/html/$(HTMLSTYLE)/cover.html
 doc/refman/styles.hva: doc/common/styles/html/$(HTMLSTYLE)/styles.hva
 	$(INSTALLLIB) $< doc/refman
 
-doc/refman/html/index.html: doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
-                        doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html
+INDEXES:= doc/refman/html/command-index.html doc/refman/html/tactic-index.html
+ALLINDEXES:= doc/refman/html/index.html $(INDEXES)
+
+$(ALLINDEXES): doc/refman/Reference-Manual.html $(REFMANPNGFILES) \
+	       doc/refman/cover.html doc/refman/styles.hva doc/refman/index.html
 	- rm -rf doc/refman/html
 	$(MKDIR) doc/refman/html
 	$(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;\
@@ -133,6 +142,14 @@ refman-quick:
 	$(HEVEA) $(HEVEAOPTS) ./Reference-Manual.tex)
 
 ######################################################################
+# Index file for CoqIDE
+######################################################################
+
+$(INDEXURLS): $(INDEXES)
+	cat $< | grep li-indexenv | grep HREF | sed -e 's@.*<TT>\(.*\)</TT>.*, <A HREF="\(.*\)">.*@\1,\2@' > $@
+
+
+######################################################################
 # Tutorial
 ######################################################################
 
@@ -183,32 +200,40 @@ doc/faq/html/index.html: doc/faq/FAQ.v.html
 ### Standard library (browsable html format)
 
 ifdef QUICK
-doc/stdlib/html/genindex.html:
+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) $(PLUGINSVO)
-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 \
-	  -R theories Coq -R plugins Coq $(THEORIESVO:.vo=.v)  $(PLUGINSVO:.vo=.v)
-	mv doc/stdlib/html/index.html doc/stdlib/html/genindex.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
+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)
 
 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)
+doc/stdlib/Library.coqdoc.tex: $(COQDOC) $(THEORIESLIGHTVO)
+	$(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
+            -R theories Coq $(THEORIESLIGHTVO:.vo=.v) > $@
 endif
-	$(COQDOC) -q -boot --gallina --body-only --latex --stdout \
-            -R theories Coq $(THEORIESLIGHTVO:.vo=.v) >> $@
 
 doc/stdlib/Library.dvi: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Library.tex
 	(cd doc/stdlib;\
@@ -221,6 +246,34 @@ doc/stdlib/Library.pdf: $(DOCCOMMON) doc/stdlib/Library.coqdoc.tex doc/stdlib/Li
 	$(PDFLATEX) -interaction=batchmode Library;\
 	../tools/show_latex_messages -no-overfull Library.log)
 
+### Standard library (full version if you're crazy enouth to try)
+
+doc/stdlib/FullLibrary.tex: doc/stdlib/Library.tex
+	sed -e 's/Library.coqdoc/FullLibrary.coqdoc/g;s/\\begin{document}/\\newcommand{\\textlambda}{\\ensuremath{\\lambda}}\\newcommand{\\textPi}{\\ensuremath{\\Pi}}\\begin{document}/' $< > $@
+
+ifdef QUICK
+doc/stdlib/FullLibrary.coqdoc.tex:
+	$(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
+            -R theories Coq $(THEORIESVO:.vo=.v) > $@
+	sed -i "" -e 's///g' $@
+else
+doc/stdlib/FullLibrary.coqdoc.tex: $(COQDOC) $(THEORIESVO)
+	$(COQDOC) -q -boot --gallina --body-only --latex --stdout --utf8 \
+            -R theories Coq $(THEORIESVO:.vo=.v) > $@
+	sed -i "" -e 's///g' $@
+endif
+
+doc/stdlib/FullLibrary.dvi: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/FullLibrary.tex
+	(cd doc/stdlib;\
+	$(LATEX) -interaction=batchmode FullLibrary;\
+	$(LATEX) -interaction=batchmode FullLibrary > /dev/null;\
+	../tools/show_latex_messages -no-overfull FullLibrary.log)
+
+doc/stdlib/FullLibrary.pdf: $(DOCCOMMON) doc/stdlib/FullLibrary.coqdoc.tex doc/stdlib/FullLibrary.dvi
+	(cd doc/stdlib;\
+	$(PDFLATEX) -interaction=batchmode FullLibrary;\
+	../tools/show_latex_messages -no-overfull FullLibrary.log)
+
 ######################################################################
 # Tutorial on inductive types
 ######################################################################
@@ -242,22 +295,12 @@ doc/RecTutorial/RecTutorial.html: doc/RecTutorial/RecTutorial.tex
 	(cd doc/RecTutorial; $(HEVEA) $(HEVEAOPTS) RecTutorial)
 
 ######################################################################
-# Index file for CoqIDE
-######################################################################
-
-# Not robust, improve...
-ide/index_urls.txt: doc/refman/html/index.html
-	@ 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
 ######################################################################
 
-.PHONY: install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-url
+.PHONY: install-doc install-doc-meta install-doc-html install-doc-printable install-doc-index-urls
 
-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-urls
 
 install-doc-meta:
 	$(MKDIR) $(FULLDOCDIR)
@@ -284,9 +327,9 @@ install-doc-printable:
 	$(INSTALLLIB) doc/RecTutorial/RecTutorial.ps $(FULLDOCDIR)/ps/RecTutorial.ps
 	$(INSTALLLIB) doc/faq/FAQ.v.ps $(FULLDOCDIR)/ps/FAQ.ps
 
-install-doc-index-url:
+install-doc-index-urls:
 	$(MKDIR) $(FULLDOCDIR)/ps $(FULLDOCDIR)/pdf
-	$(INSTALLLIB) doc/refman/html/index_urls.txt \
+	$(INSTALLLIB) $(INDEXURLS) \
 		$(FULLDOCDIR)/html/refman 
 
 # For emacs: