1 %% |
|
2 %% macros for Isabelle generated LaTeX output |
|
3 %% |
|
4 |
|
5 %%% Simple document preparation (based on theory token language and symbols) |
|
6 |
|
7 % isabelle environments |
|
8 |
|
9 \newcommand{\isabellecontext}{UNKNOWN} |
|
10 \newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}} |
|
11 |
|
12 \newcommand{\isastyle}{\UNDEF} |
|
13 \newcommand{\isastylett}{\UNDEF} |
|
14 \newcommand{\isastyleminor}{\UNDEF} |
|
15 \newcommand{\isastyleminortt}{\UNDEF} |
|
16 \newcommand{\isastylescript}{\UNDEF} |
|
17 \newcommand{\isastyletext}{\normalsize\normalfont\rmfamily} |
|
18 \newcommand{\isastyletxt}{\normalfont\rmfamily} |
|
19 \newcommand{\isastylecmt}{\normalfont\rmfamily} |
|
20 |
|
21 \newcommand{\isaspacing}{% |
|
22 \sfcode 42 1000 % . |
|
23 \sfcode 63 1000 % ? |
|
24 \sfcode 33 1000 % ! |
|
25 \sfcode 58 1000 % : |
|
26 \sfcode 59 1000 % ; |
|
27 \sfcode 44 1000 % , |
|
28 } |
|
29 |
|
30 %symbol markup -- \emph achieves decent spacing via italic corrections |
|
31 \newcommand{\isamath}[1]{\emph{$#1$}} |
|
32 \newcommand{\isatext}[1]{\emph{#1}} |
|
33 \DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}} |
|
34 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
|
35 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
|
36 \DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript} |
|
37 \DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup} |
|
38 \DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript} |
|
39 \DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup} |
|
40 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
|
41 |
|
42 \newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}} |
|
43 |
|
44 \newdimen\isa@parindent\newdimen\isa@parskip |
|
45 |
|
46 \newenvironment{isabellebody}{% |
|
47 \isamarkuptrue\par% |
|
48 \isa@parindent\parindent\parindent0pt% |
|
49 \isa@parskip\parskip\parskip0pt% |
|
50 \isaspacing\isastyle}{\par} |
|
51 |
|
52 \newenvironment{isabellebodytt}{% |
|
53 \isamarkuptrue\par% |
|
54 \isa@parindent\parindent\parindent0pt% |
|
55 \isa@parskip\parskip\parskip0pt% |
|
56 \isaspacing\isastylett}{\par} |
|
57 |
|
58 \newenvironment{isabelle} |
|
59 {\begin{trivlist}\begin{isabellebody}\item\relax} |
|
60 {\end{isabellebody}\end{trivlist}} |
|
61 |
|
62 \newenvironment{isabellett} |
|
63 {\begin{trivlist}\begin{isabellebodytt}\item\relax} |
|
64 {\end{isabellebodytt}\end{trivlist}} |
|
65 |
|
66 \newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}} |
|
67 \newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}} |
|
68 |
|
69 \newcommand{\isaindent}[1]{\hphantom{#1}} |
|
70 \newcommand{\isanewline}{\mbox{}\par\mbox{}} |
|
71 \newcommand{\isasep}{} |
|
72 \newcommand{\isadigit}[1]{#1} |
|
73 |
|
74 \newcommand{\isachardefaults}{% |
|
75 \def\isacharbell{\isamath{\bigbox}}%requires stmaryrd |
|
76 \chardef\isacharbang=`\!% |
|
77 \chardef\isachardoublequote=`\"% |
|
78 \chardef\isachardoublequoteopen=`\"% |
|
79 \chardef\isachardoublequoteclose=`\"% |
|
80 \chardef\isacharhash=`\#% |
|
81 \chardef\isachardollar=`\$% |
|
82 \chardef\isacharpercent=`\%% |
|
83 \chardef\isacharampersand=`\&% |
|
84 \chardef\isacharprime=`\'% |
|
85 \chardef\isacharparenleft=`\(% |
|
86 \chardef\isacharparenright=`\)% |
|
87 \chardef\isacharasterisk=`\*% |
|
88 \chardef\isacharplus=`\+% |
|
89 \chardef\isacharcomma=`\,% |
|
90 \chardef\isacharminus=`\-% |
|
91 \chardef\isachardot=`\.% |
|
92 \chardef\isacharslash=`\/% |
|
93 \chardef\isacharcolon=`\:% |
|
94 \chardef\isacharsemicolon=`\;% |
|
95 \chardef\isacharless=`\<% |
|
96 \chardef\isacharequal=`\=% |
|
97 \chardef\isachargreater=`\>% |
|
98 \chardef\isacharquery=`\?% |
|
99 \chardef\isacharat=`\@% |
|
100 \chardef\isacharbrackleft=`\[% |
|
101 \chardef\isacharbackslash=`\\% |
|
102 \chardef\isacharbrackright=`\]% |
|
103 \chardef\isacharcircum=`\^% |
|
104 \chardef\isacharunderscore=`\_% |
|
105 \def\isacharunderscorekeyword{\_}% |
|
106 \chardef\isacharbackquote=`\`% |
|
107 \chardef\isacharbackquoteopen=`\`% |
|
108 \chardef\isacharbackquoteclose=`\`% |
|
109 \chardef\isacharbraceleft=`\{% |
|
110 \chardef\isacharbar=`\|% |
|
111 \chardef\isacharbraceright=`\}% |
|
112 \chardef\isachartilde=`\~% |
|
113 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}% |
|
114 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright}% |
|
115 \def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% |
|
116 \def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% |
|
117 } |
|
118 |
|
119 |
|
120 % keyword and section markup |
|
121 |
|
122 \newcommand{\isakeyword}[1] |
|
123 {\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}% |
|
124 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}} |
|
125 \newcommand{\isacommand}[1]{\isakeyword{#1}} |
|
126 |
|
127 \newcommand{\isakeywordcontrol}[1] |
|
128 {\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}} |
|
129 |
|
130 \newcommand{\isamarkupchapter}[1]{\chapter{#1}} |
|
131 \newcommand{\isamarkupsection}[1]{\section{#1}} |
|
132 \newcommand{\isamarkupsubsection}[1]{\subsection{#1}} |
|
133 \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}} |
|
134 \newcommand{\isamarkupparagraph}[1]{\paragraph{#1}} |
|
135 \newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}} |
|
136 |
|
137 \newif\ifisamarkup |
|
138 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi} |
|
139 \newcommand{\isaendpar}{\par\medskip} |
|
140 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar} |
|
141 \newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}} |
|
142 \newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}} |
|
143 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} |
|
144 |
|
145 |
|
146 % styles |
|
147 |
|
148 \def\isabellestyle#1{\csname isabellestyle#1\endcsname} |
|
149 |
|
150 \newcommand{\isabellestyledefault}{% |
|
151 \def\isastyle{\small\normalfont\ttfamily\slshape}% |
|
152 \def\isastylett{\small\normalfont\ttfamily}% |
|
153 \def\isastyleminor{\small\normalfont\ttfamily\slshape}% |
|
154 \def\isastyleminortt{\small\normalfont\ttfamily}% |
|
155 \def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}% |
|
156 \isachardefaults% |
|
157 } |
|
158 \isabellestyledefault |
|
159 |
|
160 \newcommand{\isabellestylett}{% |
|
161 \def\isastyle{\small\normalfont\ttfamily}% |
|
162 \def\isastylett{\small\normalfont\ttfamily}% |
|
163 \def\isastyleminor{\small\normalfont\ttfamily}% |
|
164 \def\isastyleminortt{\small\normalfont\ttfamily}% |
|
165 \def\isastylescript{\footnotesize\normalfont\ttfamily}% |
|
166 \isachardefaults% |
|
167 } |
|
168 |
|
169 \newcommand{\isabellestyleit}{% |
|
170 \def\isastyle{\small\normalfont\itshape}% |
|
171 \def\isastylett{\small\normalfont\ttfamily}% |
|
172 \def\isastyleminor{\normalfont\itshape}% |
|
173 \def\isastyleminortt{\normalfont\ttfamily}% |
|
174 \def\isastylescript{\footnotesize\normalfont\itshape}% |
|
175 \isachardefaults% |
|
176 \def\isacharunderscorekeyword{\mbox{-}}% |
|
177 \def\isacharbang{\isamath{!}}% |
|
178 \def\isachardoublequote{}% |
|
179 \def\isachardoublequoteopen{}% |
|
180 \def\isachardoublequoteclose{}% |
|
181 \def\isacharhash{\isamath{\#}}% |
|
182 \def\isachardollar{\isamath{\$}}% |
|
183 \def\isacharpercent{\isamath{\%}}% |
|
184 \def\isacharampersand{\isamath{\&}}% |
|
185 \def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}% |
|
186 \def\isacharparenleft{\isamath{(}}% |
|
187 \def\isacharparenright{\isamath{)}}% |
|
188 \def\isacharasterisk{\isamath{*}}% |
|
189 \def\isacharplus{\isamath{+}}% |
|
190 \def\isacharcomma{\isamath{\mathord,}}% |
|
191 \def\isacharminus{\isamath{-}}% |
|
192 \def\isachardot{\isamath{\mathord.}}% |
|
193 \def\isacharslash{\isamath{/}}% |
|
194 \def\isacharcolon{\isamath{\mathord:}}% |
|
195 \def\isacharsemicolon{\isamath{\mathord;}}% |
|
196 \def\isacharless{\isamath{<}}% |
|
197 \def\isacharequal{\isamath{=}}% |
|
198 \def\isachargreater{\isamath{>}}% |
|
199 \def\isacharat{\isamath{@}}% |
|
200 \def\isacharbrackleft{\isamath{[}}% |
|
201 \def\isacharbackslash{\isamath{\backslash}}% |
|
202 \def\isacharbrackright{\isamath{]}}% |
|
203 \def\isacharunderscore{\mbox{-}}% |
|
204 \def\isacharbraceleft{\isamath{\{}}% |
|
205 \def\isacharbar{\isamath{\mid}}% |
|
206 \def\isacharbraceright{\isamath{\}}}% |
|
207 \def\isachartilde{\isamath{{}\sp{\sim}}}% |
|
208 \def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% |
|
209 \def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% |
|
210 \def\isacharverbatimopen{\isamath{\langle\!\langle}}% |
|
211 \def\isacharverbatimclose{\isamath{\rangle\!\rangle}}% |
|
212 } |
|
213 |
|
214 \newcommand{\isabellestyleliteral}{% |
|
215 \isabellestyleit% |
|
216 \def\isacharunderscore{\_}% |
|
217 \def\isacharunderscorekeyword{\_}% |
|
218 \chardef\isacharbackquoteopen=`\`% |
|
219 \chardef\isacharbackquoteclose=`\`% |
|
220 } |
|
221 |
|
222 \newcommand{\isabellestyleliteralunderscore}{% |
|
223 \isabellestyleliteral% |
|
224 \def\isacharunderscore{\textunderscore}% |
|
225 \def\isacharunderscorekeyword{\textunderscore}% |
|
226 } |
|
227 |
|
228 \newcommand{\isabellestylesl}{% |
|
229 \isabellestyleit% |
|
230 \def\isastyle{\small\normalfont\slshape}% |
|
231 \def\isastylett{\small\normalfont\ttfamily}% |
|
232 \def\isastyleminor{\normalfont\slshape}% |
|
233 \def\isastyleminortt{\normalfont\ttfamily}% |
|
234 \def\isastylescript{\footnotesize\normalfont\slshape}% |
|
235 } |
|
236 |
|
237 |
|
238 % cancel text |
|
239 |
|
240 \usepackage[normalem]{ulem} |
|
241 \newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}} |
|
242 |
|
243 |
|
244 % tagged regions |
|
245 |
|
246 %plain TeX version of comment package -- much faster! |
|
247 \let\isafmtname\fmtname\def\fmtname{plain} |
|
248 \usepackage{comment} |
|
249 \let\fmtname\isafmtname |
|
250 |
|
251 \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}} |
|
252 |
|
253 \newcommand{\isakeeptag}[1]% |
|
254 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}} |
|
255 \newcommand{\isadroptag}[1]% |
|
256 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}} |
|
257 \newcommand{\isafoldtag}[1]% |
|
258 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}} |
|
259 |
|
260 \isakeeptag{document} |
|
261 \isakeeptag{theory} |
|
262 \isakeeptag{proof} |
|
263 \isakeeptag{ML} |
|
264 \isakeeptag{visible} |
|
265 \isadroptag{invisible} |
|
266 \isakeeptag{important} |
|
267 \isakeeptag{unimportant} |
|
268 |
|
269 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{} |
|