1.1 --- /dev/null Thu Jan 01 00:00:00 1970 +0000
1.2 +++ b/src/Tools/isac/Doc/isabelle.sty Wed Mar 11 15:25:52 2020 +0100
1.3 @@ -0,0 +1,269 @@
1.4 +%%
1.5 +%% macros for Isabelle generated LaTeX output
1.6 +%%
1.7 +
1.8 +%%% Simple document preparation (based on theory token language and symbols)
1.9 +
1.10 +% isabelle environments
1.11 +
1.12 +\newcommand{\isabellecontext}{UNKNOWN}
1.13 +\newcommand{\setisabellecontext}[1]{\def\isabellecontext{#1}}
1.14 +
1.15 +\newcommand{\isastyle}{\UNDEF}
1.16 +\newcommand{\isastylett}{\UNDEF}
1.17 +\newcommand{\isastyleminor}{\UNDEF}
1.18 +\newcommand{\isastyleminortt}{\UNDEF}
1.19 +\newcommand{\isastylescript}{\UNDEF}
1.20 +\newcommand{\isastyletext}{\normalsize\normalfont\rmfamily}
1.21 +\newcommand{\isastyletxt}{\normalfont\rmfamily}
1.22 +\newcommand{\isastylecmt}{\normalfont\rmfamily}
1.23 +
1.24 +\newcommand{\isaspacing}{%
1.25 + \sfcode 42 1000 % .
1.26 + \sfcode 63 1000 % ?
1.27 + \sfcode 33 1000 % !
1.28 + \sfcode 58 1000 % :
1.29 + \sfcode 59 1000 % ;
1.30 + \sfcode 44 1000 % ,
1.31 +}
1.32 +
1.33 +%symbol markup -- \emph achieves decent spacing via italic corrections
1.34 +\newcommand{\isamath}[1]{\emph{$#1$}}
1.35 +\newcommand{\isatext}[1]{\emph{#1}}
1.36 +\DeclareRobustCommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isaspacing\isastylescript##1}}}
1.37 +\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
1.38 +\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
1.39 +\DeclareRobustCommand{\isactrlbsub}{\emph\bgroup\math{}\sb\bgroup\mbox\bgroup\isaspacing\isastylescript}
1.40 +\DeclareRobustCommand{\isactrlesub}{\egroup\egroup\endmath\egroup}
1.41 +\DeclareRobustCommand{\isactrlbsup}{\emph\bgroup\math{}\sp\bgroup\mbox\bgroup\isaspacing\isastylescript}
1.42 +\DeclareRobustCommand{\isactrlesup}{\egroup\egroup\endmath\egroup}
1.43 +\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}}
1.44 +
1.45 +\newenvironment{isaantiq}{{\isacharat\isacharbraceleft}}{{\isacharbraceright}}
1.46 +
1.47 +\newdimen\isa@parindent\newdimen\isa@parskip
1.48 +
1.49 +\newenvironment{isabellebody}{%
1.50 +\isamarkuptrue\par%
1.51 +\isa@parindent\parindent\parindent0pt%
1.52 +\isa@parskip\parskip\parskip0pt%
1.53 +\isaspacing\isastyle}{\par}
1.54 +
1.55 +\newenvironment{isabellebodytt}{%
1.56 +\isamarkuptrue\par%
1.57 +\isa@parindent\parindent\parindent0pt%
1.58 +\isa@parskip\parskip\parskip0pt%
1.59 +\isaspacing\isastylett}{\par}
1.60 +
1.61 +\newenvironment{isabelle}
1.62 +{\begin{trivlist}\begin{isabellebody}\item\relax}
1.63 +{\end{isabellebody}\end{trivlist}}
1.64 +
1.65 +\newenvironment{isabellett}
1.66 +{\begin{trivlist}\begin{isabellebodytt}\item\relax}
1.67 +{\end{isabellebodytt}\end{trivlist}}
1.68 +
1.69 +\newcommand{\isa}[1]{\emph{\isaspacing\isastyleminor #1}}
1.70 +\newcommand{\isatt}[1]{\emph{\isaspacing\isastyleminortt #1}}
1.71 +
1.72 +\newcommand{\isaindent}[1]{\hphantom{#1}}
1.73 +\newcommand{\isanewline}{\mbox{}\par\mbox{}}
1.74 +\newcommand{\isasep}{}
1.75 +\newcommand{\isadigit}[1]{#1}
1.76 +
1.77 +\newcommand{\isachardefaults}{%
1.78 +\def\isacharbell{\isamath{\bigbox}}%requires stmaryrd
1.79 +\chardef\isacharbang=`\!%
1.80 +\chardef\isachardoublequote=`\"%
1.81 +\chardef\isachardoublequoteopen=`\"%
1.82 +\chardef\isachardoublequoteclose=`\"%
1.83 +\chardef\isacharhash=`\#%
1.84 +\chardef\isachardollar=`\$%
1.85 +\chardef\isacharpercent=`\%%
1.86 +\chardef\isacharampersand=`\&%
1.87 +\chardef\isacharprime=`\'%
1.88 +\chardef\isacharparenleft=`\(%
1.89 +\chardef\isacharparenright=`\)%
1.90 +\chardef\isacharasterisk=`\*%
1.91 +\chardef\isacharplus=`\+%
1.92 +\chardef\isacharcomma=`\,%
1.93 +\chardef\isacharminus=`\-%
1.94 +\chardef\isachardot=`\.%
1.95 +\chardef\isacharslash=`\/%
1.96 +\chardef\isacharcolon=`\:%
1.97 +\chardef\isacharsemicolon=`\;%
1.98 +\chardef\isacharless=`\<%
1.99 +\chardef\isacharequal=`\=%
1.100 +\chardef\isachargreater=`\>%
1.101 +\chardef\isacharquery=`\?%
1.102 +\chardef\isacharat=`\@%
1.103 +\chardef\isacharbrackleft=`\[%
1.104 +\chardef\isacharbackslash=`\\%
1.105 +\chardef\isacharbrackright=`\]%
1.106 +\chardef\isacharcircum=`\^%
1.107 +\chardef\isacharunderscore=`\_%
1.108 +\def\isacharunderscorekeyword{\_}%
1.109 +\chardef\isacharbackquote=`\`%
1.110 +\chardef\isacharbackquoteopen=`\`%
1.111 +\chardef\isacharbackquoteclose=`\`%
1.112 +\chardef\isacharbraceleft=`\{%
1.113 +\chardef\isacharbar=`\|%
1.114 +\chardef\isacharbraceright=`\}%
1.115 +\chardef\isachartilde=`\~%
1.116 +\def\isacharverbatimopen{\isacharbraceleft\isacharasterisk}%
1.117 +\def\isacharverbatimclose{\isacharasterisk\isacharbraceright}%
1.118 +\def\isacartoucheopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
1.119 +\def\isacartoucheclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
1.120 +}
1.121 +
1.122 +
1.123 +% keyword and section markup
1.124 +
1.125 +\newcommand{\isakeyword}[1]
1.126 +{\emph{\normalfont\bfseries\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
1.127 +\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
1.128 +\newcommand{\isacommand}[1]{\isakeyword{#1}}
1.129 +
1.130 +\newcommand{\isakeywordcontrol}[1]
1.131 +{\emph{\normalfont\bfseries\itshape\def\isacharunderscore{\isacharunderscorekeyword}#1\,}}
1.132 +
1.133 +\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
1.134 +\newcommand{\isamarkupsection}[1]{\section{#1}}
1.135 +\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
1.136 +\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
1.137 +\newcommand{\isamarkupparagraph}[1]{\paragraph{#1}}
1.138 +\newcommand{\isamarkupsubparagraph}[1]{\subparagraph{#1}}
1.139 +
1.140 +\newif\ifisamarkup
1.141 +\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}
1.142 +\newcommand{\isaendpar}{\par\medskip}
1.143 +\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
1.144 +\newenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}}{\end{isapar}}
1.145 +\newenvironment{isamarkuptxt}{\par\isastyletxt\begin{isapar}}{\end{isapar}}
1.146 +\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
1.147 +
1.148 +
1.149 +% styles
1.150 +
1.151 +\def\isabellestyle#1{\csname isabellestyle#1\endcsname}
1.152 +
1.153 +\newcommand{\isabellestyledefault}{%
1.154 +\def\isastyle{\small\normalfont\ttfamily\slshape}%
1.155 +\def\isastylett{\small\normalfont\ttfamily}%
1.156 +\def\isastyleminor{\small\normalfont\ttfamily\slshape}%
1.157 +\def\isastyleminortt{\small\normalfont\ttfamily}%
1.158 +\def\isastylescript{\footnotesize\normalfont\ttfamily\slshape}%
1.159 +\isachardefaults%
1.160 +}
1.161 +\isabellestyledefault
1.162 +
1.163 +\newcommand{\isabellestylett}{%
1.164 +\def\isastyle{\small\normalfont\ttfamily}%
1.165 +\def\isastylett{\small\normalfont\ttfamily}%
1.166 +\def\isastyleminor{\small\normalfont\ttfamily}%
1.167 +\def\isastyleminortt{\small\normalfont\ttfamily}%
1.168 +\def\isastylescript{\footnotesize\normalfont\ttfamily}%
1.169 +\isachardefaults%
1.170 +}
1.171 +
1.172 +\newcommand{\isabellestyleit}{%
1.173 +\def\isastyle{\small\normalfont\itshape}%
1.174 +\def\isastylett{\small\normalfont\ttfamily}%
1.175 +\def\isastyleminor{\normalfont\itshape}%
1.176 +\def\isastyleminortt{\normalfont\ttfamily}%
1.177 +\def\isastylescript{\footnotesize\normalfont\itshape}%
1.178 +\isachardefaults%
1.179 +\def\isacharunderscorekeyword{\mbox{-}}%
1.180 +\def\isacharbang{\isamath{!}}%
1.181 +\def\isachardoublequote{}%
1.182 +\def\isachardoublequoteopen{}%
1.183 +\def\isachardoublequoteclose{}%
1.184 +\def\isacharhash{\isamath{\#}}%
1.185 +\def\isachardollar{\isamath{\$}}%
1.186 +\def\isacharpercent{\isamath{\%}}%
1.187 +\def\isacharampersand{\isamath{\&}}%
1.188 +\def\isacharprime{\isamath{\mskip2mu{'}\mskip-2mu}}%
1.189 +\def\isacharparenleft{\isamath{(}}%
1.190 +\def\isacharparenright{\isamath{)}}%
1.191 +\def\isacharasterisk{\isamath{*}}%
1.192 +\def\isacharplus{\isamath{+}}%
1.193 +\def\isacharcomma{\isamath{\mathord,}}%
1.194 +\def\isacharminus{\isamath{-}}%
1.195 +\def\isachardot{\isamath{\mathord.}}%
1.196 +\def\isacharslash{\isamath{/}}%
1.197 +\def\isacharcolon{\isamath{\mathord:}}%
1.198 +\def\isacharsemicolon{\isamath{\mathord;}}%
1.199 +\def\isacharless{\isamath{<}}%
1.200 +\def\isacharequal{\isamath{=}}%
1.201 +\def\isachargreater{\isamath{>}}%
1.202 +\def\isacharat{\isamath{@}}%
1.203 +\def\isacharbrackleft{\isamath{[}}%
1.204 +\def\isacharbackslash{\isamath{\backslash}}%
1.205 +\def\isacharbrackright{\isamath{]}}%
1.206 +\def\isacharunderscore{\mbox{-}}%
1.207 +\def\isacharbraceleft{\isamath{\{}}%
1.208 +\def\isacharbar{\isamath{\mid}}%
1.209 +\def\isacharbraceright{\isamath{\}}}%
1.210 +\def\isachartilde{\isamath{{}\sp{\sim}}}%
1.211 +\def\isacharbackquoteopen{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\langle$}}}%
1.212 +\def\isacharbackquoteclose{\isatext{\raise.3ex\hbox{$\scriptscriptstyle\rangle$}}}%
1.213 +\def\isacharverbatimopen{\isamath{\langle\!\langle}}%
1.214 +\def\isacharverbatimclose{\isamath{\rangle\!\rangle}}%
1.215 +}
1.216 +
1.217 +\newcommand{\isabellestyleliteral}{%
1.218 +\isabellestyleit%
1.219 +\def\isacharunderscore{\_}%
1.220 +\def\isacharunderscorekeyword{\_}%
1.221 +\chardef\isacharbackquoteopen=`\`%
1.222 +\chardef\isacharbackquoteclose=`\`%
1.223 +}
1.224 +
1.225 +\newcommand{\isabellestyleliteralunderscore}{%
1.226 +\isabellestyleliteral%
1.227 +\def\isacharunderscore{\textunderscore}%
1.228 +\def\isacharunderscorekeyword{\textunderscore}%
1.229 +}
1.230 +
1.231 +\newcommand{\isabellestylesl}{%
1.232 +\isabellestyleit%
1.233 +\def\isastyle{\small\normalfont\slshape}%
1.234 +\def\isastylett{\small\normalfont\ttfamily}%
1.235 +\def\isastyleminor{\normalfont\slshape}%
1.236 +\def\isastyleminortt{\normalfont\ttfamily}%
1.237 +\def\isastylescript{\footnotesize\normalfont\slshape}%
1.238 +}
1.239 +
1.240 +
1.241 +% cancel text
1.242 +
1.243 +\usepackage[normalem]{ulem}
1.244 +\newcommand{\isamarkupcancel}[1]{\isa{\xout{#1}}}
1.245 +
1.246 +
1.247 +% tagged regions
1.248 +
1.249 +%plain TeX version of comment package -- much faster!
1.250 +\let\isafmtname\fmtname\def\fmtname{plain}
1.251 +\usepackage{comment}
1.252 +\let\fmtname\isafmtname
1.253 +
1.254 +\newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}
1.255 +
1.256 +\newcommand{\isakeeptag}[1]%
1.257 +{\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}
1.258 +\newcommand{\isadroptag}[1]%
1.259 +{\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}
1.260 +\newcommand{\isafoldtag}[1]%
1.261 +{\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}
1.262 +
1.263 +\isakeeptag{document}
1.264 +\isakeeptag{theory}
1.265 +\isakeeptag{proof}
1.266 +\isakeeptag{ML}
1.267 +\isakeeptag{visible}
1.268 +\isadroptag{invisible}
1.269 +\isakeeptag{important}
1.270 +\isakeeptag{unimportant}
1.271 +
1.272 +\IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}