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