author | kleing |
Mon, 29 Dec 2003 06:07:44 +0100 | |
changeset 14332 | fd3535af90ab |
parent 14234 | 9590df3c5f2a |
child 14345 | 3023d90dc59e |
permissions | -rw-r--r-- |
wenzelm@7709 | 1 |
%% |
wenzelm@9818 | 2 |
%% Author: Markus Wenzel, TU Muenchen |
wenzelm@9818 | 3 |
%% License: GPL (GNU GENERAL PUBLIC LICENSE) |
wenzelm@7709 | 4 |
%% |
wenzelm@7709 | 5 |
%% macros for Isabelle generated LaTeX output |
wenzelm@7709 | 6 |
%% |
wenzelm@7709 | 7 |
|
wenzelm@9913 | 8 |
%%% Simple document preparation (based on theory token language and symbols) |
wenzelm@7709 | 9 |
|
wenzelm@8714 | 10 |
% isabelle environments |
wenzelm@7788 | 11 |
|
wenzelm@9913 | 12 |
\newcommand{\isabellecontext}{UNKNOWN} |
wenzelm@9913 | 13 |
|
wenzelm@9657 | 14 |
\newcommand{\isastyle}{\small\tt\slshape} |
wenzelm@9669 | 15 |
\newcommand{\isastyleminor}{\small\tt\slshape} |
wenzelm@10220 | 16 |
\newcommand{\isastylescript}{\footnotesize\tt\slshape} |
wenzelm@9657 | 17 |
\newcommand{\isastyletext}{\normalsize\rm} |
wenzelm@9657 | 18 |
\newcommand{\isastyletxt}{\rm} |
wenzelm@9657 | 19 |
\newcommand{\isastylecmt}{\rm} |
wenzelm@8713 | 20 |
|
wenzelm@10220 | 21 |
%symbol markup -- \emph achieves decent spacing via italic corrections |
wenzelm@10220 | 22 |
\newcommand{\isamath}[1]{\emph{$#1$}} |
wenzelm@10220 | 23 |
\newcommand{\isatext}[1]{\emph{#1}} |
wenzelm@10220 | 24 |
\newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}} |
wenzelm@10260 | 25 |
\newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
wenzelm@10260 | 26 |
\newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
kleing@14234 | 27 |
\newcommand{\isactrlisub}[1]{\emph{\isascriptstyle${}\sb{#1}$}} |
kleing@14234 | 28 |
\newcommand{\isactrlisup}[1]{\emph{\isascriptstyle${}\sp{#1}$}} |
wenzelm@11573 | 29 |
\newcommand{\isactrlbold}[1]{{\bfseries\upshape\boldmath#1}} |
wenzelm@10220 | 30 |
|
kleing@14332 | 31 |
% somewhat hackish: spanning sub/super scripts (\<^bsub>..\<^esub>) |
kleing@14332 | 32 |
\newcommand{\isactrlbsub}{% |
kleing@14332 | 33 |
\def\isatext##1{\isastylescript##1}\begin{math}_\bgroup} |
kleing@14332 | 34 |
\newcommand{\isactrlesub}{\egroup\end{math}} |
kleing@14332 | 35 |
\newcommand{\isactrlbsup}{% |
kleing@14332 | 36 |
\def\isatext##1{\isastylescript##1}\begin{math}^\bgroup} |
kleing@14332 | 37 |
\newcommand{\isactrlesup}{\egroup\end{math}} |
kleing@14332 | 38 |
|
wenzelm@8713 | 39 |
\newdimen\isa@parindent\newdimen\isa@parskip |
wenzelm@9657 | 40 |
|
wenzelm@9702 | 41 |
\newenvironment{isabellebody}{% |
wenzelm@11863 | 42 |
\isamarkuptrue\par% |
wenzelm@9702 | 43 |
\isa@parindent\parindent\parindent0pt% |
wenzelm@8713 | 44 |
\isa@parskip\parskip\parskip0pt% |
wenzelm@10470 | 45 |
\isastyle}{\par} |
wenzelm@9702 | 46 |
|
wenzelm@9702 | 47 |
\newenvironment{isabelle} |
wenzelm@10422 | 48 |
{\begin{trivlist}\begin{isabellebody}\item\relax} |
wenzelm@10422 | 49 |
{\end{isabellebody}\end{trivlist}} |
wenzelm@8713 | 50 |
|
wenzelm@9669 | 51 |
\newcommand{\isa}[1]{\emph{\isastyleminor #1}} |
wenzelm@8714 | 52 |
|
wenzelm@10949 | 53 |
\newcommand{\isaindent}[1]{\hphantom{#1}} |
kleing@13933 | 54 |
\newcommand{\isanewline}{\mbox{}\par\mbox{}} |
wenzelm@9669 | 55 |
\newcommand{\isadigit}[1]{#1} |
wenzelm@7752 | 56 |
|
wenzelm@9669 | 57 |
\chardef\isacharbang=`\! |
wenzelm@9669 | 58 |
\chardef\isachardoublequote=`\" |
wenzelm@9657 | 59 |
\chardef\isacharhash=`\# |
wenzelm@9657 | 60 |
\chardef\isachardollar=`\$ |
wenzelm@9657 | 61 |
\chardef\isacharpercent=`\% |
wenzelm@9657 | 62 |
\chardef\isacharampersand=`\& |
wenzelm@9657 | 63 |
\chardef\isacharprime=`\' |
wenzelm@9657 | 64 |
\chardef\isacharparenleft=`\( |
wenzelm@9657 | 65 |
\chardef\isacharparenright=`\) |
wenzelm@9657 | 66 |
\chardef\isacharasterisk=`\* |
wenzelm@9669 | 67 |
\chardef\isacharplus=`\+ |
wenzelm@9669 | 68 |
\chardef\isacharcomma=`\, |
wenzelm@9657 | 69 |
\chardef\isacharminus=`\- |
wenzelm@9669 | 70 |
\chardef\isachardot=`\. |
wenzelm@9669 | 71 |
\chardef\isacharslash=`\/ |
wenzelm@9669 | 72 |
\chardef\isacharcolon=`\: |
wenzelm@9669 | 73 |
\chardef\isacharsemicolon=`\; |
wenzelm@9657 | 74 |
\chardef\isacharless=`\< |
wenzelm@9669 | 75 |
\chardef\isacharequal=`\= |
wenzelm@9657 | 76 |
\chardef\isachargreater=`\> |
wenzelm@9669 | 77 |
\chardef\isacharquery=`\? |
wenzelm@9669 | 78 |
\chardef\isacharat=`\@ |
wenzelm@9657 | 79 |
\chardef\isacharbrackleft=`\[ |
wenzelm@9657 | 80 |
\chardef\isacharbackslash=`\\ |
wenzelm@9657 | 81 |
\chardef\isacharbrackright=`\] |
wenzelm@9657 | 82 |
\chardef\isacharcircum=`\^ |
wenzelm@9657 | 83 |
\chardef\isacharunderscore=`\_ |
wenzelm@9669 | 84 |
\chardef\isacharbackquote=`\` |
wenzelm@9657 | 85 |
\chardef\isacharbraceleft=`\{ |
wenzelm@9657 | 86 |
\chardef\isacharbar=`\| |
wenzelm@9657 | 87 |
\chardef\isacharbraceright=`\} |
wenzelm@9657 | 88 |
\chardef\isachartilde=`\~ |
wenzelm@7788 | 89 |
|
wenzelm@7797 | 90 |
|
wenzelm@7797 | 91 |
% keyword and section markup |
wenzelm@7788 | 92 |
|
wenzelm@9710 | 93 |
\newcommand{\isakeywordcharunderscore}{\_} |
wenzelm@9669 | 94 |
\newcommand{\isakeyword}[1] |
wenzelm@9710 | 95 |
{\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}% |
wenzelm@9669 | 96 |
\def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}} |
wenzelm@9669 | 97 |
\newcommand{\isacommand}[1]{\isakeyword{#1}} |
wenzelm@7758 | 98 |
|
wenzelm@8501 | 99 |
\newcommand{\isamarkupheader}[1]{\section{#1}} |
wenzelm@7752 | 100 |
\newcommand{\isamarkupchapter}[1]{\chapter{#1}} |
wenzelm@7752 | 101 |
\newcommand{\isamarkupsection}[1]{\section{#1}} |
wenzelm@7752 | 102 |
\newcommand{\isamarkupsubsection}[1]{\subsection{#1}} |
wenzelm@7752 | 103 |
\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}} |
wenzelm@7752 | 104 |
\newcommand{\isamarkupsect}[1]{\section{#1}} |
wenzelm@7752 | 105 |
\newcommand{\isamarkupsubsect}[1]{\subsection{#1}} |
wenzelm@7752 | 106 |
\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}} |
wenzelm@8662 | 107 |
|
wenzelm@11863 | 108 |
\newif\ifisamarkup |
wenzelm@11863 | 109 |
\newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi} |
wenzelm@10586 | 110 |
\newcommand{\isaendpar}{\par\medskip} |
wenzelm@10586 | 111 |
\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar} |
wenzelm@9657 | 112 |
\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}} |
wenzelm@9657 | 113 |
\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}} |
wenzelm@9657 | 114 |
\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}} |
wenzelm@9657 | 115 |
|
wenzelm@9657 | 116 |
|
wenzelm@10024 | 117 |
% alternative styles |
wenzelm@9657 | 118 |
|
wenzelm@9657 | 119 |
\newcommand{\isabellestyle}{} |
wenzelm@9669 | 120 |
\def\isabellestyle#1{\csname isabellestyle#1\endcsname} |
wenzelm@9657 | 121 |
|
wenzelm@10024 | 122 |
\newcommand{\isabellestylett}{% |
wenzelm@10024 | 123 |
\renewcommand{\isastyle}{\small\tt}% |
wenzelm@10188 | 124 |
\renewcommand{\isastyleminor}{\small\tt}% |
wenzelm@10220 | 125 |
\renewcommand{\isastylescript}{\footnotesize\tt}% |
wenzelm@10024 | 126 |
} |
wenzelm@9669 | 127 |
\newcommand{\isabellestyleit}{% |
wenzelm@9669 | 128 |
\renewcommand{\isastyle}{\small\it}% |
wenzelm@9669 | 129 |
\renewcommand{\isastyleminor}{\it}% |
wenzelm@10220 | 130 |
\renewcommand{\isastylescript}{\footnotesize\it}% |
wenzelm@9725 | 131 |
\renewcommand{\isakeywordcharunderscore}{\mbox{-}}% |
wenzelm@10220 | 132 |
\renewcommand{\isacharbang}{\isamath{!}}% |
wenzelm@9669 | 133 |
\renewcommand{\isachardoublequote}{}% |
wenzelm@10220 | 134 |
\renewcommand{\isacharhash}{\isamath{\#}}% |
wenzelm@10220 | 135 |
\renewcommand{\isachardollar}{\isamath{\$}}% |
wenzelm@10220 | 136 |
\renewcommand{\isacharpercent}{\isamath{\%}}% |
wenzelm@10220 | 137 |
\renewcommand{\isacharampersand}{\isamath{\&}}% |
wenzelm@10220 | 138 |
\renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}% |
wenzelm@10220 | 139 |
\renewcommand{\isacharparenleft}{\isamath{(}}% |
wenzelm@10220 | 140 |
\renewcommand{\isacharparenright}{\isamath{)}}% |
wenzelm@10220 | 141 |
\renewcommand{\isacharasterisk}{\isamath{*}}% |
wenzelm@10220 | 142 |
\renewcommand{\isacharplus}{\isamath{+}}% |
wenzelm@10220 | 143 |
\renewcommand{\isacharcomma}{\isamath{\mathord,}}% |
wenzelm@10220 | 144 |
\renewcommand{\isacharminus}{\isamath{-}}% |
wenzelm@10220 | 145 |
\renewcommand{\isachardot}{\isamath{\mathord.}}% |
wenzelm@10220 | 146 |
\renewcommand{\isacharslash}{\isamath{/}}% |
wenzelm@10220 | 147 |
\renewcommand{\isacharcolon}{\isamath{\mathord:}}% |
wenzelm@10220 | 148 |
\renewcommand{\isacharsemicolon}{\isamath{\mathord;}}% |
wenzelm@10220 | 149 |
\renewcommand{\isacharless}{\isamath{<}}% |
wenzelm@10220 | 150 |
\renewcommand{\isacharequal}{\isamath{=}}% |
wenzelm@10220 | 151 |
\renewcommand{\isachargreater}{\isamath{>}}% |
wenzelm@10220 | 152 |
\renewcommand{\isacharat}{\isamath{@}}% |
wenzelm@10220 | 153 |
\renewcommand{\isacharbrackleft}{\isamath{[}}% |
wenzelm@10220 | 154 |
\renewcommand{\isacharbrackright}{\isamath{]}}% |
wenzelm@9725 | 155 |
\renewcommand{\isacharunderscore}{\mbox{-}}% |
wenzelm@10220 | 156 |
\renewcommand{\isacharbraceleft}{\isamath{\{}}% |
wenzelm@10220 | 157 |
\renewcommand{\isacharbar}{\isamath{\mid}}% |
wenzelm@10220 | 158 |
\renewcommand{\isacharbraceright}{\isamath{\}}}% |
wenzelm@10260 | 159 |
\renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}% |
wenzelm@9657 | 160 |
} |
wenzelm@9657 | 161 |
|
wenzelm@9975 | 162 |
\newcommand{\isabellestylesl}{% |
wenzelm@9975 | 163 |
\isabellestyleit% |
wenzelm@9975 | 164 |
\renewcommand{\isastyle}{\small\sl}% |
wenzelm@9975 | 165 |
\renewcommand{\isastyleminor}{\sl}% |
wenzelm@10220 | 166 |
\renewcommand{\isastylescript}{\footnotesize\sl}% |
wenzelm@9975 | 167 |
} |