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