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