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