1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
|
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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}}
%BEGIN LATEX
\renewcommand{\contentsname}{%
\protect\setheaders{Table of contents}Table of contents}
\renewcommand{\bibname}{\protect\setheaders{Bibliography}%
\protect\RefManCutCommand{BEGINBIBLIO=\thepage}%
\protect\addcontentsline{toc}{chapter}{Bibliography}Bibliography}
%END LATEX
%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% 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{\errindexbis}[2]{\texttt{#1}\index[error]{#2}}
\newcommand{\ttindex}[1]{\index{#1@\texttt{#1}}}
\makeatother
% The following code creates another command \@indexlabel, which,
% along with Hevea's \@currentlabel serves to store the current values
% of counters. However, \@currentlabel keeps the value of counters
% incremented by \refstepcounter (see the definition of
% \refstepcounter in latexcommon.hva), which includes chapter and
% section counters, as well as theorems, \items, etc. On the other
% hand, \@indexlabel keeps only the values of sectioning counters.
% This is done by redefining the sectioning commands.
%HEVEA \newcommand{\@indexlabel}{}
%HEVEA \let\oldchapter=\chapter
%HEVEA \let\oldsection=\section
%HEVEA \let\oldsubsection=\subsection
%HEVEA \let\oldsubsubsection=\subsubsection
%HEVEA \let\oldparagraph=\paragraph
%HEVEA \let\oldsubparagraph=\subparagraph
%HEVEA \renewcommand{\chapter}[1]{\oldchapter{#1}\let\@indexlabel=\@currentlabel}
%HEVEA \renewcommand{\section}[1]{\oldsection{#1}\let\@indexlabel=\@currentlabel}
%HEVEA \renewcommand{\subsection}[1]{\oldsubsection{#1}\let\@indexlabel=\@currentlabel}
%HEVEA \renewcommand{\subsubsection}[1]{\oldsubsubsection{#1}\let\@indexlabel=\@currentlabel}
%HEVEA \renewcommand{\paragraph}[1]{\oldparagraph{#1}\let\@indexlabel=\@currentlabel}
%HEVEA \renewcommand{\subparagraph}[1]{\oldsubparagraph{#1}\let\@indexlabel=\@currentlabel}
% The only difference of the following command with the original one
% defined in index.hva is that the latter uses \@currentlabel instead
% of \@indexlabel
% Also, for some reason, the following command produces an error if
% not given on one line. Need to submit to Hevea developers.
%HEVEA \renewcommand{\index}[2][default]{\if@refs\sbox{\@indexbox}{\@indexwrite[#1]{#2}{\@indexlabel}}\@locname{\usebox{\@indexbox}}{}\fi}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% For the Addendum table of contents
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
\newcommand{\aauthor}[1]{{\LARGE \bf #1} \bigskip \bigskip \bigskip}
\makeatletter
%BEGIN LATEX
\newcommand{\atableofcontents}{\section*{Contents}\@starttoc{atoc}}
\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}}
%END LATEX
%HEVEA \newcommand{\atableofcontents}{}
%HEVEA \newcommand{\achapter}[1]{\chapter{#1}}
%HEVEA \newcommand{\asection}{\section}
%HEVEA \newcommand{\asubsection}{\subsection}
%HEVEA \newcommand{\asubsubsection}{\subsubsection}
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
% Reference-Manual.sh is generated to cut the Postscript
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%\@starttoc{sh}
%BEGIN LATEX
\newwrite\RefManCut@out%
\immediate\openout\RefManCut@out\jobname.sh
\newcommand{\RefManCutCommand}[1]{%
\immediate\write\RefManCut@out{#1}}
\newcommand{\RefManCutClose}{%
\immediate\closeout\RefManCut@out}
%END LATEX
%%% Local Variables:
%%% mode: latex
%%% TeX-master: "Reference-Manual"
%%% End:
|
