Add "make full-stdlib" to make all the doc in pdf as ask by bug 2395

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13976 85f007b7-540e-0410-9357-904b9bb8a0f7

3 files changed, 37 insertions, 4 deletions

diff --git a/CHANGES b/CHANGES
index 19edf585e..29e5b3d68 100644
--- a/CHANGES
+++ b/CHANGES
@@ -23,7 +23,7 @@ Tactics
 - New tactics constr_eq, is_evar and has_evar.
 - Remove the two-argument variant of "decide equality".
 - New experimental tactical "timeout <n> <tac>". Since <n> is a time
-  in second for the moment, this feature should rather be avoided 
+  in second for the moment, this feature should rather be avoided
   in scripts meant to be machine-independent.
 
 Vernacular commands
@@ -85,6 +85,8 @@ Internal infrastructure
   for both make and ocamlbuild, etc.
 - Support of cross-compilation via mingw toward Windows, contact P. Letouzey
   for more informations.
+- new Makefile rules mli-doc to make html of mli in dev/doc/html and
+  full-stdlib to get a HUGE pdf with all the stdlib.
 
 Extraction
 
diff --git a/Makefile b/Makefile
index 10b102932..33ee0490c 100644
--- a/Makefile
+++ b/Makefile
@@ -182,9 +182,9 @@ docclean:
 	doc/*/*.hatoc doc/*/*.haux doc/*/*.hcomind doc/*/*.herrind doc/*/*.hidx doc/*/*.hind \
 	doc/*/*.htacind doc/*/*.htoc doc/*/*.v.html
 	rm -f doc/stdlib/index-list.html doc/stdlib/index-body.html \
-	  doc/stdlib/Library.coqdoc.tex doc/stdlib/library.files \
-	  doc/stdlib/library.files.ls
-	rm -f doc/*/*.ps doc/*/*.pdf 
+	  doc/stdlib/*Library.coqdoc.tex doc/stdlib/library.files \
+	  doc/stdlib/library.files.ls doc/stdlib/FullLibrary.tex
+	rm -f doc/*/*.ps doc/*/*.pdf
 	rm -rf doc/refman/html doc/stdlib/html doc/faq/html doc/tutorial/tutorial.v.html
 	rm -f doc/refman/euclid.ml doc/refman/euclid.mli
 	rm -f doc/refman/heapsort.ml doc/refman/heapsort.mli
diff --git a/Makefile.doc b/Makefile.doc
index 584e25394..dc3ae8b5f 100644
--- a/Makefile.doc
+++ b/Makefile.doc
@@ -36,6 +36,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 \
@@ -229,6 +232,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
 ######################################################################