Initial revision

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

1 files changed, 86 insertions, 0 deletions

diff --git a/doc/headers.tex b/doc/headers.tex
new file mode 100644
index 0000000000..11664861f1
--- /dev/null
+++ b/doc/headers.tex
@@ -0,0 +1,86 @@
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% File title.tex
+% Pretty Headers
+% And commands for multiple indexes
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\usepackage{fancyhdr}
+
+\setlength{\headheight}{14pt}
+
+\pagestyle{fancyplain}
+
+\newcommand{\coqfooter}{\tiny Coq Reference Manual, V\coqversion{}, \today}
+
+\cfoot{}
+\lfoot[{\coqfooter}]{}
+\rfoot[]{{\coqfooter}}
+
+\newcommand{\setheaders}[1]{
+\rhead[\fancyplain{}{\textbf{#1}}]{\fancyplain{}{\thepage}}
+\lhead[\fancyplain{}{\thepage}]{\fancyplain{}{\textbf{#1}}}
+}
+\newcommand{\defaultheaders}{
+\rhead[\fancyplain{}{\leftmark}]{\fancyplain{}{\thepage}}
+\lhead[\fancyplain{}{\thepage}]{\fancyplain{}{\rightmark}}
+}
+
+\renewcommand{\chaptermark}[1]{\markboth{{\bf \thechapter~#1}}{}}
+\renewcommand{\sectionmark}[1]{\markright{\thesection~#1}}
+\renewcommand{\contentsname}{%
+\protect\setheaders{Table of contents}Table of contents}
+\renewcommand{\bibname}{\protect\setheaders{Bibliography}%
+\protect\addtocontents{sh}{BEGINBIBLIO=\thepage}%
+\protect\addcontentsline{toc}{chapter}{Bibliography}Bibliography}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% For the Addendum table of contents
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\newcommand{\atableofcontents}{\section*{Contents}\@starttoc{atoc}}
+\newcommand{\aauthor}[1]{{\LARGE \bf #1} \bigskip \bigskip \bigskip}
+\newcommand{\achapter}[1]{
+  \chapter{#1}\addcontentsline{atoc}{chapter}{#1}}
+\newcommand{\asection}[1]{
+  \section{#1}\addcontentsline{atoc}{section}{#1}}
+\newcommand{\asubsection}[1]{
+  \subsection{#1}\addcontentsline{atoc}{subsection}{#1}}
+\newcommand{\asubsubsection}[1]{
+  \subsubsection{#1}\addcontentsline{atoc}{subsubsection}{#1}}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Reference-Manual.sh is generated to cut the Postscript
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\@starttoc{sh}
+
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+% Commands for indexes
+%%%%%%%%%%%%%%%%%%%%%%%%%%%%
+\usepackage{index}
+\makeindex
+\newindex{tactic}{tacidx}{tacind}{%
+\protect\setheaders{Tactics Index}%
+\protect\addcontentsline{toc}{chapter}{Tactics Index}Tactics Index}
+
+\newindex{command}{comidx}{comind}{%
+\protect\setheaders{Vernacular Commands Index}%
+\protect\addcontentsline{toc}{chapter}{Vernacular Commands Index}%
+Vernacular Commands Index}
+
+\newindex{error}{erridx}{errind}{%
+\protect\setheaders{Index of Error Messages}%
+\protect\addcontentsline{toc}{chapter}{Index of Error Messages}Index of Error Messages}
+
+\renewindex{default}{idx}{ind}{%
+\protect\addcontentsline{toc}{chapter}{Global Index}%
+\protect\setheaders{Global Index}Global Index}
+
+\newcommand{\tacindex}[1]{%
+\index{#1@\texttt{#1}}\index[tactic]{#1@\texttt{#1}}}
+\newcommand{\comindex}[1]{%
+\index{#1@\texttt{#1}}\index[command]{#1@\texttt{#1}}}
+\newcommand{\errindex}[1]{\texttt{#1}\index[error]{#1}}
+\newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}}
+
+%%% Local Variables: 
+%%% mode: latex
+%%% TeX-master: "Reference-Manual"
+%%% End: