1% =====================================================================
2% Macros for typesetting hol reference manual entries
3% =====================================================================
4
5% ---------------------------------------------------------------------
6% boolean flag for verbose printing of reference manual typesetting
7% ---------------------------------------------------------------------
8
9\newif\ifverboseref
10\verbosereffalse                          % don't be verbose
11
12% ---------------------------------------------------------------------
13% Macro for generating right-hand page running titles.
14% ---------------------------------------------------------------------
15
16\makeatletter
17
18\def\mkhead{\futurelet\@t\chsize}
19\def\chsize#1.{\ifx a\@t \markright{{\protect\bf #1}}\else
20               \ifx b\@t \markright{{\protect\bf #1}}\else
21               \ifx c\@t \markright{{\protect\bf #1}}\else
22               \ifx d\@t \markright{{\protect\bf #1}}\else
23               \ifx e\@t \markright{{\protect\bf #1}}\else
24               \ifx f\@t \markright{{\protect\bf #1}}\else
25               \ifx g\@t \markright{{\protect\bf #1}}\else
26               \ifx h\@t \markright{{\protect\bf #1}}\else
27               \ifx i\@t \markright{{\protect\bf #1}}\else
28               \ifx j\@t \markright{{\protect\bf #1}}\else
29               \ifx k\@t \markright{{\protect\bf #1}}\else
30               \ifx l\@t \markright{{\protect\bf #1}}\else
31               \ifx m\@t \markright{{\protect\bf #1}}\else
32               \ifx n\@t \markright{{\protect\bf #1}}\else
33               \ifx o\@t \markright{{\protect\bf #1}}\else
34               \ifx p\@t \markright{{\protect\bf #1}}\else
35               \ifx q\@t \markright{{\protect\bf #1}}\else
36               \ifx r\@t \markright{{\protect\bf #1}}\else
37               \ifx s\@t \markright{{\protect\bf #1}}\else
38               \ifx t\@t \markright{{\protect\bf #1}}\else
39               \ifx u\@t \markright{{\protect\bf #1}}\else
40               \ifx v\@t \markright{{\protect\bf #1}}\else
41               \ifx w\@t \markright{{\protect\bf #1}}\else
42               \ifx z\@t \markright{{\protect\bf #1}}\else
43               \ifx y\@t \markright{{\protect\bf #1}}\else
44               \ifx z\@t \markright{{\protect\bf #1}}\else
45               \markright{{\protect\small\bf #1}}\fi
46               \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi\fi
47               \fi\fi\fi\fi\fi\fi\fi\fi\fi\fi}
48
49\makeatother
50
51% ---------------------------------------------------------------------
52% \DOC{<object>}  : start a manual entry for <object>.
53% ---------------------------------------------------------------------
54
55\newcommand{\DOC}[2]%
56{\bigskip
57 {\ifverboseref{\def\_{\string_}\typeout{Typesetting: #1}}\fi}
58 \bgroup\samepage               % ended after \TYPE
59 \mkhead #1.
60 \begin{flushleft}
61 \begin{tabular}{|c|}\hline
62 \begin{minipage}{\minipagewidth}
63 \bigskip
64 {\def\_{\char'137}\LARGE\tt #2}\index{#1@{\tt #1}}
65 \bigskip
66 \end{minipage}\\ \hline
67 \end{tabular}
68 \end{flushleft}
69 \vskip10pt}
70
71% ---------------------------------------------------------------------
72% \setseps = set the spacing parameters for above and below displays
73% ---------------------------------------------------------------------
74\def\setseps{\partopsep=0mm\topsep=12pt plus2pt minus2pt}
75
76% ---------------------------------------------------------------------
77% flag for typesetting SEEALSO list
78% ---------------------------------------------------------------------
79\newif\ifseealso
80\seealsofalse                     % start false.
81
82% ---------------------------------------------------------------------
83% \TYPE {<thing>} : {<type>}
84% ---------------------------------------------------------------------
85\def\TYPE{\noindent}
86
87% ---------------------------------------------------------------------
88% Commands for parts of a \DOC:
89%    \SYNOPSIS
90%    \DESCRIBE
91%    \FAILURE
92%    \EXAMPLE
93%    \USES
94%    \SEEALSO
95% ---------------------------------------------------------------------
96
97\newcommand\beforeskip{\vspace{12pt plus4pt minus4pt}}
98
99\newcommand{\SYNOPSIS}%
100{\beforeskip\leftline{\large\bf Synopsis}\nobreak\noindent}
101
102\newcommand{\DESCRIBE}%
103{\beforeskip\leftline{\large\bf Description}\nobreak\noindent}
104
105\newcommand{\FAILURE}%
106{\beforeskip\leftline{\large\bf Failure}\nobreak\noindent}
107
108\newcommand{\EXAMPLE}%
109{\beforeskip\leftline{\large\bf Example}\nobreak\noindent}
110
111\newcommand{\USES}%
112{\beforeskip\leftline{\large\bf Uses}\nobreak\noindent}
113
114\newcommand{\COMMENTS}%
115{\beforeskip\leftline{\large\bf Comments}\nobreak\noindent}
116
117\newcommand{\SEEALSO}%
118{\beforeskip\seealsotrue\leftline{\large\bf See also}\nobreak\noindent%
119\bgroup\raggedright\small\tt\catcode`\_=12}
120
121% ---------------------------------------------------------------------
122% \ENDDOC = do nothing, but close off the group started by \SEEALSO
123% ---------------------------------------------------------------------
124
125\newcommand{\ENDDOC}{\ifseealso \egroup\seealsofalse \else \relax \fi}
126
127% =====================================================================
128% Commands for typesetting theorems
129% =====================================================================
130
131\makeatletter
132
133% ---------------------------------------------------------------------
134% define \@xboxverb<thing>\ENDTHEOREM to mean <thing>\ENDTHEOREM
135% ---------------------------------------------------------------------
136
137\begingroup \catcode `|=0 \catcode `[= 1
138\catcode`]=2 \catcode `\{=12 \catcode `\}=12
139\catcode`\\=12 |gdef|@xboxverb#1\ENDTHEOREM[#1|ENDTHEOREM]
140|endgroup
141
142% ---------------------------------------------------------------------
143% \bboxverb<thing> = <thing> in a verbatim box 5mm from left margin
144% ---------------------------------------------------------------------
145
146\def\@boxverb{\bgroup\leftskip=5mm\parindent\z@
147\parfillskip=\@flushglue\parskip\z@
148\obeylines\small\tt \catcode``=13 \@noligs \let\do\@makeother \dospecials}
149
150\def\boxverb{\@boxverb \frenchspacing\@vobeyspaces \@xboxverb}
151
152% ---------------------------------------------------------------------
153% \ENDTHEOREM just finishes off the group (and kick page if necessary)
154% ---------------------------------------------------------------------
155
156\def\ENDTHEOREM{\egroup\filbreak}
157
158% ---------------------------------------------------------------------
159% \THEOREM <name> <thy> ... \ENDTHEOREM = typeset a theorem
160% ---------------------------------------------------------------------
161
162\def\THEOREM #1 #2 {
163 \index{#1@{\tt #1}}
164   \vspace{4mm plus2mm minus1mm}
165\noindent {\def\_{{\char'137}}\small\tt #1}\quad({\small\tt #2}) \par \boxverb
166}
167
168\makeatother
169
170% ---------------------------------------------------------------------
171% The theory name \none = italic "none"
172% ---------------------------------------------------------------------
173
174\def\none{{\it none}}
175