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