File: layout.sty

package info (click to toggle)
hol88 2.02.19940316-35
  • links: PTS
  • area: main
  • in suites: bullseye, buster, sid
  • size: 65,988 kB
  • ctags: 21,623
  • sloc: ml: 199,939; ansic: 9,666; sh: 7,118; makefile: 6,095; lisp: 2,747; yacc: 894; sed: 201; cpp: 87; awk: 5
file content (287 lines) | stat: -rw-r--r-- 11,106 bytes parent folder | download | duplicates (6)
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
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
% =====================================================================
%
% LaTeX style file for the HOL system manual
%
% =====================================================================

% ---------------------------------------------------------------------
% BOOLEAN FLAG FOR PAPER SIZE.
%
% set:   \Afourtrue    to make paper size A4
%        \Afourfalse   to make paper size 8.5 x 11 inches
% ---------------------------------------------------------------------

\newif\ifAfour
\Afourtrue

% ---------------------------------------------------------------------
% PAPER SIZE  (latex overrides these anyway)
%
% TeX expects 1 inch margins all around.
%    * a4 (european paper) is exactly 297mm high by 210mm wide
%    * 8.5x11 (american paper) is exactly 279.4mm high by 215.9mm wide
%
% 1 inch = 25.4 mm
% ---------------------------------------------------------------------

\ifAfour \hsize=159.2truemm \else \hsize=165.1truemm \fi
\ifAfour \vsize=246.2truemm \else \vsize=228.6truemm \fi

% ---------------------------------------------------------------------
% PAGE LAYOUT  
% ---------------------------------------------------------------------

\textwidth 160truemm
\textheight 225truemm

% ---------------------------------------------------------------------
% POSITION ON PAPER  Adjusted for local conditions (see \Afour above)
% ---------------------------------------------------------------------

% Double sided
\ifAfour \oddsidemargin=6.6truemm \else \oddsidemargin=8.55truemm \fi
\ifAfour \evensidemargin=-7.4truemm \else \evensidemargin=-3.45truemm \fi

% Single Sided 
%\ifAfour \oddsidemargin=6.6truemm \else \oddsidemargin=8.55truemm \fi
%\ifAfour \evensidemargin=6.6truemm \else \evensidemargin=8.55truemm \fi

\ifAfour \topmargin 1truemm \else \topmargin -4truemm \fi

% ---------------------------------------------------------------------
% MATH INDENTATION.  = \tabcolsep + three small verbatim spaces  (!)
% ---------------------------------------------------------------------
\setlength{\mathindent}{\tabcolsep}
%\addtolength{\mathindent}{\the\fontdimen2\elvtt}
%\addtolength{\mathindent}{\the\fontdimen2\elvtt}
%\addtolength{\mathindent}{\the\fontdimen2\elvtt}

% ---------------------------------------------------------------------
% HEAD: spacing to match header macro below.
% ---------------------------------------------------------------------
\headheight 16pt
\headsep 20pt 

% ---------------------------------------------------------------------
% FOOT: page number in 12 point font
% ---------------------------------------------------------------------
\footheight 12pt
\footskip 13mm

% ---------------------------------------------------------------------
% INDENTATION: 4mm indentation
% --------------------------------------------------------------------- 
\parindent 4mm

% ---------------------------------------------------------------------
% FOOTNOTES: footnotes are in 10 point font.
%
% put 12+1-1 points between text and rule
% put 10pt between at start of footnote
% foot note rule is 40mm long
% ---------------------------------------------------------------------
\skip\footins 12pt plus 2pt minus 2pt
\footnotesep 10pt
\def\footnoterule{\kern-3\p@ \hrule width 40mm \kern 2.6\p@}

% ---------------------------------------------------------------------
% FLOATS
% ---------------------------------------------------------------------
\floatsep 12pt plus 2pt minus 2pt
\textfloatsep  20pt plus 2pt minus 4pt
\intextsep 12pt plus 2pt minus 2pt
\@maxsep 20pt

% ---------------------------------------------------------------------
% Make "@" a "letter" for definitions that follow
% ---------------------------------------------------------------------
\makeatletter   

% ---------------------------------------------------------------------
% CHAPTER HEADINGS (deriving from Larry Paulson)
% ---------------------------------------------------------------------

\def\@rulehead#1{\hrule height1pt \vskip 14pt \huge \bf 
   #1 \vskip 14pt\hrule height1pt}

\def\@makechapterhead#1{ { \parindent 0pt 
\ifnum \c@secnumdepth >\m@ne \raggedright\large\bf \@chapapp{} \thechapter\par
 \vskip 8pt \fi \raggedright \@rulehead{#1} \par 
 \nobreak \vskip 50pt } }

\def\@makeschapterhead#1{ { \parindent 0pt {\large\bf\phantom{Chapter}} \par
   \vskip 8pt \raggedright 
 \@rulehead{#1} \par \nobreak \vskip 50pt } }


% ---------------------------------------------------------------------
% PAGE FOOT, on pages that start a new chapter
% ---------------------------------------------------------------------

\def\ps@plain{\let\@mkboth\@gobbletwo
     \def\@oddhead{}\def\@oddfoot{\rm\bf\hfil\thepage
     \hfil}\def\@evenhead{}\let\@evenfoot\@oddfoot}

% ---------------------------------------------------------------------
% PAGE HEADINGS
% ---------------------------------------------------------------------

\def\ps@headings{\def\@oddfoot{}\def\@evenfoot{}\def
  \@evenhead{\vbox{\hbox to \textwidth{\bf\thepage\hfil\bf\leftmark
	}\vskip-\prevdepth\vskip 4.5pt\hrule height0.9pt}}\def
  \@oddhead{\vbox{\hbox to \textwidth{\bf\rightmark\hfil\bf
	\thepage}\vskip-\prevdepth\vskip 4.5pt\hrule height0.9pt}}\def
  \chaptermark##1{\markboth {{\ifnum \c@secnumdepth
>\m@ne
\@chapapp\ \thechapter. \ \fi ##1}}{}}\def\sectionmark##1{\markright
{{\ifnum \c@secnumdepth >\z@
\thesection. \ \fi ##1}}}}

% ---------------------------------------------------------------------
% Table of contents
% ---------------------------------------------------------------------
\def\tableofcontents{\@restonecolfalse\if@twocolumn\@restonecoltrue\onecolumn
 \fi\chapter*{Contents\@mkboth{Contents}{Contents}}
 \@starttoc{toc}\if@restonecol\twocolumn\fi}

% ---------------------------------------------------------------------
% Part
% ---------------------------------------------------------------------
\def\part{\cleardoublepage \thispagestyle{empty} \if@twocolumn \onecolumn
\@tempswatrue \else \@tempswafalse \fi \hbox{}\vfil \bgroup \centering
\secdef\@part\@spart} 

\def\@endpart{\par\egroup \vfil\newpage \if@twoside \hbox{}
\thispagestyle{empty} 
 \newpage 
 \fi \if@tempswa \twocolumn \fi} 

% ---------------------------------------------------------------------
% REFERENCES
%
% (1) For references in each volume use:
%
%        \begin{thebibliography} ... \end{thebibliography}
%
%     This makes the references a new chapter.
%
% (2) For case study references, also use:
%
%        \begin{thebibliography} ... \end{thebibliography}
%
%     This makes the references in a case study an unumbered section.
%
% NOTE: references in case studies should have different names than
%       those in the body of the tutorial.  (I.e. different \bibitem name).
% ---------------------------------------------------------------------

\def\thebibliography#1{\chapter*{References\@mkboth
 {References}{References}} \addcontentsline{toc}{chapter}{References}
 \list {[\arabic{enumi}]}{\settowidth\labelwidth{[#1]}\leftmargin\labelwidth
 \advance\leftmargin\labelsep
 \usecounter{enumi}}
 \def\newblock{\hskip .11em plus .33em minus -.07em}
 \sloppy
 \sfcode`\.=1000\relax}
\let\endthebibliography=\endlist

\ps@headings  %to override previous

% ---------------------------------------------------------------------
% To make the index
% ---------------------------------------------------------------------
\def\theindex{\@restonecoltrue\if@twocolumn\@restonecolfalse\fi
\columnseprule \z@
\columnsep 35pt\twocolumn[\@makeschapterhead{Index}]
 \@mkboth{Index}{Index}\thispagestyle{plain}
 \addcontentsline{toc}{chapter}{Index}
 \parindent\z@
 \parskip\z@ plus .3pt\relax\let\item\@idxitem}
\def\@idxitem{\par\hangindent 40pt}
\def\subitem{\par\hangindent 40pt \hspace*{20pt}}
\def\subsubitem{\par\hangindent 40pt \hspace*{30pt}}
\def\endtheindex{\if@restonecol\onecolumn\else\clearpage\fi}

% ---------------------------------------------------------------------
% Other Indexing commands
%
% autoindex is defined for indexing the thing in \DOC{thing}. 
% It translates \_ in thing to \string \_.
% ---------------------------------------------------------------------

\def\makeindex{\if@filesw \newwrite\@indexfile
  \immediate\openout\@indexfile=\jobname.idx
  \def\index{\@bsphack\begingroup
             \def\protect####1{\string####1\space}\@sanitize
             \@wrindex\@indexfile}
  \def\autoindex{\@bsphack\begingroup
             \def\protect####1{\string####1\space}
             \def\_{\string\_}\@sanitize
             \@wrindex\@indexfile}\typeout
  {Writing index file \jobname.idx }\fi}

\def\@wrindex#1#2{\let\thepage\relax
   \xdef\@gtempa{\write#1{\string
      \indexentry{#2}{\thepage}}}\endgroup\@gtempa
   \if@nobreak \ifvmode\nobreak\fi\fi\@esphack}

\def\index{\@bsphack\begingroup \@sanitize\@index}
\def\autoindex{\@bsphack\begingroup \@sanitize\@index}

\def\@index#1{\endgroup\@esphack}

% ---------------------------------------------------------------------
% Enumeration with Roman numerals: one-level enumeration only
% ---------------------------------------------------------------------

\newcount\@myenumdepth \@myenumdepth = 0
\@definecounter{myenumi}

%\newenvironment{myenumerate}{\begin{enumerate}}{\end{enumerate}}
%  \renewcommand{\theenumi}{\roman{enumi}}
%  \renewcommand{\labelenumi}{(\roman{enumi})}}{\end{enumerate}}

\def\myenumerate{\ifnum \@myenumdepth >0 \@toodeep\else
      \advance\@myenumdepth \@ne 
       \list{(\roman{myenumi})}{\usecounter{myenumi}
            \settowidth{\labelwidth}{(iii)}
            \setlength{\leftmargin}{\labelwidth}
            \addtolength{\leftmargin}{\labelsep}
            \addtolength{\leftmargin}{\mathindent}
            \def\makelabel##1{\hss\llap{##1}}}\fi}

\let\endmyenumerate =\endlist


% ---------------------------------------------------------------------
% Enumerate envoronment for proofs in drules.tex
% ---------------------------------------------------------------------

\def\proof{\ifnum \@enumdepth >0 \@toodeep\else
      \advance\@enumdepth \@ne 
      \edef\@enumctr{enum\romannumeral\the\@enumdepth}\list
      {\csname label\@enumctr\endcsname}{\usecounter
        {\@enumctr}\setlength{\itemsep}{0.0mm}
        \setlength{\baselineskip}{13pt}
        \def\makelabel##1{\hss\llap{##1}}}\fi}

\let\endproof =\endlist

% ---------------------------------------------------------------------
% Make "@" an "other" again
% ---------------------------------------------------------------------
\makeatother



% ---------------------------------------------------------------------
% Preliminary settings etc.
% ---------------------------------------------------------------------

\renewcommand{\topfraction}{0.8}	  % 0.8 of the top page can be fig.
\renewcommand{\bottomfraction}{0.8}	  % 0.8 of the bottom page can be fig.
\renewcommand{\textfraction}{0.1}	  % 0.1 of the page must contain text
\setcounter{totalnumber}{4}	 	  % max of 4 figures per page
\setcounter{secnumdepth}{3}		  % number sections down to level 3
\setcounter{tocdepth}{2}		  % toc contains numbers to level 2
\flushbottom				  % text extends right to the bottom