From 7ff1810bafc981ee774c431e1c7f5b99d2700cd7 Mon Sep 17 00:00:00 2001 From: marche Date: Tue, 2 Dec 2003 15:46:21 +0000 Subject: plus de pb avec referencemanual.sh git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@8375 85f007b7-540e-0410-9357-904b9bb8a0f7 --- doc/.cvsignore | 1 + doc/AddRefMan-pre.tex | 2 +- doc/Makefile | 14 +++++++------- doc/RefMan-uti.tex | 2 +- doc/Reference-Manual.tex | 13 +++++++------ doc/Setoid.tex | 5 +++++ doc/headers.tex | 10 ++++++++-- 7 files changed, 30 insertions(+), 17 deletions(-) (limited to 'doc') diff --git a/doc/.cvsignore b/doc/.cvsignore index 4b0319acf..a6109f3d0 100644 --- a/doc/.cvsignore +++ b/doc/.cvsignore @@ -1,3 +1,4 @@ +version.tex *.blg *.ind *.ilg diff --git a/doc/AddRefMan-pre.tex b/doc/AddRefMan-pre.tex index 44af92025..d467b84e6 100644 --- a/doc/AddRefMan-pre.tex +++ b/doc/AddRefMan-pre.tex @@ -1,4 +1,4 @@ -\addtocontents{sh}{BEGINADDENDUM=\thepage} +\RefManCutCommand{BEGINADDENDUM=\thepage} \coverpage{Addenddum to the Reference Manual}{\ } \addcontentsline{toc}{part}{Additional documentation} \setheaders{Presentation of the Addendum} diff --git a/doc/Makefile b/doc/Makefile index 8ab0db0e9..6f7f1fc70 100644 --- a/doc/Makefile +++ b/doc/Makefile @@ -288,29 +288,29 @@ Tutorial.v.pdf: ./title.tex Tutorial.v.tex Reference-Manual.ps: Reference-Manual.dvi Reference-Manual.dvi: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib - rm -f Reference-Manual.sh + #rm -f Reference-Manual.sh $(LATEX) Reference-Manual - rm Reference-Manual.sh + #rm Reference-Manual.sh $(BIBTEX) Reference-Manual $(LATEX) Reference-Manual - rm Reference-Manual.sh + #rm Reference-Manual.sh $(BIBTEX) Reference-Manual $(LATEX) Reference-Manual - rm Reference-Manual.sh + #rm Reference-Manual.sh $(MAKEINDEX) Reference-Manual $(MAKEINDEX) Reference-Manual.tacidx -o Reference-Manual.tacind $(MAKEINDEX) Reference-Manual.comidx -o Reference-Manual.comind $(MAKEINDEX) Reference-Manual.erridx -o Reference-Manual.errind $(LATEX) Reference-Manual - rm Reference-Manual.sh + #rm Reference-Manual.sh $(LATEX) Reference-Manual Reference-Manual.pdf: Reference-Manual.dvi - rm -f Reference-Manual.sh + #rm -f Reference-Manual.sh $(PDFLATEX) Reference-Manual.tex quick: $(INPUTS) $(REFMANFILES) $(COQTEXFILES) biblio.bib - rm -f Reference-Manual.sh + #rm -f Reference-Manual.sh $(LATEX) Reference-Manual diff --git a/doc/RefMan-uti.tex b/doc/RefMan-uti.tex index b812a3042..9d3f7b761 100755 --- a/doc/RefMan-uti.tex +++ b/doc/RefMan-uti.tex @@ -281,7 +281,7 @@ There are man pages for the commands {\tt coqdep}, {\tt gallina} and {\tt coq-tex}. Man pages are installed at installation time (see installation instructions in file {\tt INSTALL}, step 6). -\addtocontents{sh}{ENDREFMAN=\thepage} +\RefManCutCommand{ENDREFMAN=\thepage} % $Id$ diff --git a/doc/Reference-Manual.tex b/doc/Reference-Manual.tex index d4f4c4c76..493619166 100644 --- a/doc/Reference-Manual.tex +++ b/doc/Reference-Manual.tex @@ -67,19 +67,20 @@ %%SUPPRIME \include{Natural.v}% \include{Omega.v}% %%SUPPRIME \include{Program.v}% -\include{Correctness.v}% = preuve de pgms imperatifs +%%SUPPRIME \include{Correctness.v}% = preuve de pgms imperatifs \include{Extraction.v}% \include{Polynom.v}% = Ring \include{Setoid.v}% Tactique pour les setoides -\addtocontents{sh}{ENDADDENDUM=\thepage} +\RefManCutCommand{ENDADDENDUM=\thepage} \nocite{*} \bibliographystyle{plain} \bibliography{biblio} -\addtocontents{sh}{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps} -\addtocontents{sh}{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps} -\addtocontents{sh}{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-} -\addtocontents{sh}{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM} +\RefManCutCommand{psselect -q -p-$ENDREFMAN,$BEGINBIBLIO- Reference-Manual.ps Reference-Manual-base.ps} +\RefManCutCommand{psselect -q -p$BEGINADDENDUM-$ENDADDENDUM Reference-Manual.ps Reference-Manual-addendum.ps} +\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-base.dvi 1-$ENDREFMAN $BEGINBIBLIO-} +\RefManCutCommand{dviselect -i Reference-Manual.dvi -o Reference-Manual-addendum.dvi $BEGINADDENDUM-$ENDADDENDUM} +\RefManCutClose \printindex diff --git a/doc/Setoid.tex b/doc/Setoid.tex index 2659cae1e..68260e085 100644 --- a/doc/Setoid.tex +++ b/doc/Setoid.tex @@ -157,3 +157,8 @@ The arrow tells the systems in which direction the rewriting has to be done. Moreover, you can use \texttt{Rewrite} for setoid rewriting. In that case the system will check if the term you give is an equality or a setoid equivalence and do the appropriate work. + +%%% Local Variables: +%%% mode: latex +%%% TeX-master: "Reference-Manual" +%%% End: diff --git a/doc/headers.tex b/doc/headers.tex index f5b337340..cccd277c3 100644 --- a/doc/headers.tex +++ b/doc/headers.tex @@ -23,7 +23,7 @@ \renewcommand{\contentsname}{% \protect\setheaders{Table of contents}Table of contents} \renewcommand{\bibname}{\protect\setheaders{Bibliography}% -\protect\addtocontents{sh}{BEGINBIBLIO=\thepage}% +\protect\RefManCutCommand{BEGINBIBLIO=\thepage}% \protect\addcontentsline{toc}{chapter}{Bibliography}Bibliography} %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% @@ -45,7 +45,13 @@ %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% % Reference-Manual.sh is generated to cut the Postscript %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%% -\@starttoc{sh} +%\@starttoc{sh} +\newwrite\RefManCut@out% +\immediate\openout\RefManCut@out\jobname.sh +\newcommand{\RefManCutCommand}[1]{% +\immediate\write\RefManCut@out{#1}} +\newcommand{\RefManCutClose}{% +\immediate\closeout\RefManCut@out} %%%%%%%%%%%%%%%%%%%%%%%%%%%% % Commands for indexes -- cgit v1.2.3