|
1 %% |
|
2 %% |
|
3 %% |
|
4 %% macros for Isabelle generated LaTeX output |
|
5 %% |
|
6 |
|
7 %%% Simple document preparation (based on theory token language and symbols) |
|
8 |
|
9 % isabelle environments |
|
10 |
|
11 \newcommand{\isabellecontext}{UNKNOWN} |
|
12 |
|
13 \newcommand{\isastyle}{\small\tt\slshape} |
|
14 \newcommand{\isastyleminor}{\small\tt\slshape} |
|
15 \newcommand{\isastylescript}{\footnotesize\tt\slshape} |
|
16 \newcommand{\isastyletext}{\normalsize\rm} |
|
17 \newcommand{\isastyletxt}{\rm} |
|
18 \newcommand{\isastylecmt}{\rm} |
|
19 |
|
20 %symbol markup -- \emph achieves decent spacing via italic corrections |
|
21 \newcommand{\isamath}[1]{\emph{$#1$}} |
|
22 \newcommand{\isatext}[1]{\emph{#1}} |
|
23 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} |
|
24 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
|
25 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
|
26 \newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
|
27 \newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
|
28 \newcommand{\isactrlbsub}{\emph\bgroup\begin{math}{}\sb\bgroup\mbox\bgroup\isastylescript} |
|
29 \newcommand{\isactrlesub}{\egroup\egroup\end{math}\egroup} |
|
30 \newcommand{\isactrlbsup}{\emph\bgroup\begin{math}{}\sp\bgroup\mbox\bgroup\isastylescript} |
|
31 \newcommand{\isactrlesup}{\egroup\egroup\end{math}\egroup} |
|
32 \newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
|
33 \newcommand{\isactrlloc}[1]{{\bfseries\upshape\boldmath#1}} |
|
34 |
|
35 |
|
36 \newdimen\isa@parindent\newdimen\isa@parskip |
|
37 |
|
38 \newenvironment{isabellebody}{% |
|
39 \isamarkuptrue\par% |
|
40 \isa@parindent\parindent\parindent0pt% |
|
41 \isa@parskip\parskip\parskip0pt% |
|
42 \isastyle}{\par} |
|
43 |
|
44 \newenvironment{isabelle} |
|
45 {\begin{trivlist}\begin{isabellebody}\item\relax} |
|
46 {\end{isabellebody}\end{trivlist}} |
|
47 |
|
48 \newcommand{\isa}[1]{\emph{\isastyleminor #1}} |
|
49 |
|
50 \newcommand{\isaindent}[1]{\hphantom{#1}} |
|
51 \newcommand{\isanewline}{\mbox{}\par\mbox{}} |
|
52 \newcommand{\isasep}{} |
|
53 \newcommand{\isadigit}[1]{#1} |
|
54 |
|
55 \chardef\isacharbang=`\! |
|
56 \chardef\isachardoublequote=`\" |
|
57 \chardef\isachardoublequoteopen=`\" |
|
58 \chardef\isachardoublequoteclose=`\" |
|
59 \chardef\isacharhash=`\# |
|
60 \chardef\isachardollar=`\$ |
|
61 \chardef\isacharpercent=`\% |
|
62 \chardef\isacharampersand=`\& |
|
63 \chardef\isacharprime=`\' |
|
64 \chardef\isacharparenleft=`\( |
|
65 \chardef\isacharparenright=`\) |
|
66 \chardef\isacharasterisk=`\* |
|
67 \chardef\isacharplus=`\+ |
|
68 \chardef\isacharcomma=`\, |
|
69 \chardef\isacharminus=`\- |
|
70 \chardef\isachardot=`\. |
|
71 \chardef\isacharslash=`\/ |
|
72 \chardef\isacharcolon=`\: |
|
73 \chardef\isacharsemicolon=`\; |
|
74 \chardef\isacharless=`\< |
|
75 \chardef\isacharequal=`\= |
|
76 \chardef\isachargreater=`\> |
|
77 \chardef\isacharquery=`\? |
|
78 \chardef\isacharat=`\@ |
|
79 \chardef\isacharbrackleft=`\[ |
|
80 \chardef\isacharbackslash=`\\ |
|
81 \chardef\isacharbrackright=`\] |
|
82 \chardef\isacharcircum=`\^ |
|
83 \chardef\isacharunderscore=`\_ |
|
84 \chardef\isacharbackquote=`\` |
|
85 \chardef\isacharbackquoteopen=`\` |
|
86 \chardef\isacharbackquoteclose=`\` |
|
87 \chardef\isacharbraceleft=`\{ |
|
88 \chardef\isacharbar=`\| |
|
89 \chardef\isacharbraceright=`\} |
|
90 \chardef\isachartilde=`\~ |
|
91 \def\isacharverbatimopen{\isacharbraceleft\isacharasterisk} |
|
92 \def\isacharverbatimclose{\isacharasterisk\isacharbraceright} |
|
93 |
|
94 |
|
95 % keyword and section markup |
|
96 |
|
97 \newcommand{\isakeywordcharunderscore}{\_} |
|
98 \newcommand{\isakeyword}[1] |
|
99 {\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}% |
|
100 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}} |
|
101 \newcommand{\isacommand}[1]{\isakeyword{#1}} |
|
102 |
|
103 \newcommand{\isamarkupheader}[1]{\section{#1}} |
|
104 \newcommand{\isamarkupchapter}[1]{\chapter{#1}} |
|
105 \newcommand{\isamarkupsection}[1]{\section{#1}} |
|
106 \newcommand{\isamarkupsubsection}[1]{\subsection{#1}} |
|
107 \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}} |
|
108 \newcommand{\isamarkupsect}[1]{\section{#1}} |
|
109 \newcommand{\isamarkupsubsect}[1]{\subsection{#1}} |
|
110 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}} |
|
111 |
|
112 \newif\ifisamarkup |
|
113 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi} |
|
114 \newcommand{\isaendpar}{\par\medskip} |
|
115 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar} |
|
116 \newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}} |
|
117 \newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}} |
|
118 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} |
|
119 |
|
120 |
|
121 % alternative styles |
|
122 |
|
123 \newcommand{\isabellestyle}{} |
|
124 \def\isabellestyle#1{\csname isabellestyle#1\endcsname} |
|
125 |
|
126 \newcommand{\isabellestylett}{% |
|
127 \renewcommand{\isastyle}{\small\tt}% |
|
128 \renewcommand{\isastyleminor}{\small\tt}% |
|
129 \renewcommand{\isastylescript}{\footnotesize\tt}% |
|
130 } |
|
131 \newcommand{\isabellestyleit}{% |
|
132 \renewcommand{\isastyle}{\small\it}% |
|
133 \renewcommand{\isastyleminor}{\it}% |
|
134 \renewcommand{\isastylescript}{\footnotesize\it}% |
|
135 \renewcommand{\isakeywordcharunderscore}{\mbox{-}}% |
|
136 \renewcommand{\isacharbang}{\isamath{!}}% |
|
137 \renewcommand{\isachardoublequote}{}% |
|
138 \renewcommand{\isachardoublequoteopen}{}% |
|
139 \renewcommand{\isachardoublequoteclose}{}% |
|
140 \renewcommand{\isacharhash}{\isamath{\#}}% |
|
141 \renewcommand{\isachardollar}{\isamath{\$}}% |
|
142 \renewcommand{\isacharpercent}{\isamath{\%}}% |
|
143 \renewcommand{\isacharampersand}{\isamath{\&}}% |
|
144 \renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}% |
|
145 \renewcommand{\isacharparenleft}{\isamath{(}}% |
|
146 \renewcommand{\isacharparenright}{\isamath{)}}% |
|
147 \renewcommand{\isacharasterisk}{\isamath{*}}% |
|
148 \renewcommand{\isacharplus}{\isamath{+}}% |
|
149 \renewcommand{\isacharcomma}{\isamath{\mathord,}}% |
|
150 \renewcommand{\isacharminus}{\isamath{-}}% |
|
151 \renewcommand{\isachardot}{\isamath{\mathord.}}% |
|
152 \renewcommand{\isacharslash}{\isamath{/}}% |
|
153 \renewcommand{\isacharcolon}{\isamath{\mathord:}}% |
|
154 \renewcommand{\isacharsemicolon}{\isamath{\mathord;}}% |
|
155 \renewcommand{\isacharless}{\isamath{<}}% |
|
156 \renewcommand{\isacharequal}{\isamath{=}}% |
|
157 \renewcommand{\isachargreater}{\isamath{>}}% |
|
158 \renewcommand{\isacharat}{\isamath{@}}% |
|
159 \renewcommand{\isacharbrackleft}{\isamath{[}}% |
|
160 \renewcommand{\isacharbackslash}{\isamath{\backslash}}% |
|
161 \renewcommand{\isacharbrackright}{\isamath{]}}% |
|
162 \renewcommand{\isacharunderscore}{\mbox{-}}% |
|
163 \renewcommand{\isacharbraceleft}{\isamath{\{}}% |
|
164 \renewcommand{\isacharbar}{\isamath{\mid}}% |
|
165 \renewcommand{\isacharbraceright}{\isamath{\}}}% |
|
166 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}% |
|
167 \renewcommand{\isacharbackquoteopen}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}% |
|
168 \renewcommand{\isacharbackquoteclose}{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}% |
|
169 \renewcommand{\isacharverbatimopen}{\isamath{\langle\!\langle}}% |
|
170 \renewcommand{\isacharverbatimclose}{\isamath{\rangle\!\rangle}}% |
|
171 } |
|
172 |
|
173 \newcommand{\isabellestylesl}{% |
|
174 \isabellestyleit% |
|
175 \renewcommand{\isastyle}{\small\sl}% |
|
176 \renewcommand{\isastyleminor}{\sl}% |
|
177 \renewcommand{\isastylescript}{\footnotesize\sl}% |
|
178 } |
|
179 |
|
180 |
|
181 % tagged regions |
|
182 |
|
183 %plain TeX version of comment package -- much faster! |
|
184 \let\isafmtname\fmtname\def\fmtname{plain} |
|
185 \usepackage{comment} |
|
186 \let\fmtname\isafmtname |
|
187 |
|
188 \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}} |
|
189 |
|
190 \newcommand{\isakeeptag}[1]% |
|
191 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}} |
|
192 \newcommand{\isadroptag}[1]% |
|
193 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}} |
|
194 \newcommand{\isafoldtag}[1]% |
|
195 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}} |
|
196 |
|
197 \isakeeptag{theory} |
|
198 \isakeeptag{proof} |
|
199 \isakeeptag{ML} |
|
200 \isakeeptag{visible} |
|
201 \isadroptag{invisible} |
|
202 |
|
203 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{} |