wneuper/isa: lib/texinputs/isabelle.sty@30781cc78fc6

     1 %%

     2 %% Author: Markus Wenzel, TU Muenchen

     3 %%

     4 %% macros for Isabelle generated LaTeX output

     5 %%

     6 %% $Id$

     8 %%% Simple document preparation (based on theory token language and symbols)

    10 % isabelle environments

    12 \newcommand{\isabellecontext}{UNKNOWN}

    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}

    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}}

    36 \newdimen\isa@parindent\newdimen\isa@parskip

    38 \newenvironment{isabellebody}{%

    39 \isamarkuptrue\par%

    40 \isa@parindent\parindent\parindent0pt%

    41 \isa@parskip\parskip\parskip0pt%

    42 \isastyle}{\par}

    44 \newenvironment{isabelle}

    45 {\begin{trivlist}\begin{isabellebody}\item\relax}

    46 {\end{isabellebody}\end{trivlist}}

    48 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}

    50 \newcommand{\isaindent}[1]{\hphantom{#1}}

    51 \newcommand{\isanewline}{\mbox{}\par\mbox{}}

    52 \newcommand{\isasep}{} % override with e.g. \renewcommand{\isasep}{\vspace{1ex}}

    53 \newcommand{\isadigit}[1]{#1}

    55 \chardef\isacharbang=`\!

    56 \chardef\isachardoublequote=`\"

    57 \chardef\isacharhash=`\#

    58 \chardef\isachardollar=`\$

    59 \chardef\isacharpercent=`\%

    60 \chardef\isacharampersand=`\&

    61 \chardef\isacharprime=`\'

    62 \chardef\isacharparenleft=`\(

    63 \chardef\isacharparenright=`\)

    64 \chardef\isacharasterisk=`\*

    65 \chardef\isacharplus=`\+

    66 \chardef\isacharcomma=`\,

    67 \chardef\isacharminus=`\-

    68 \chardef\isachardot=`\.

    69 \chardef\isacharslash=`\/

    70 \chardef\isacharcolon=`\:

    71 \chardef\isacharsemicolon=`\;

    72 \chardef\isacharless=`\<

    73 \chardef\isacharequal=`\=

    74 \chardef\isachargreater=`\>

    75 \chardef\isacharquery=`\?

    76 \chardef\isacharat=`\@

    77 \chardef\isacharbrackleft=`\[

    78 \chardef\isacharbackslash=`\\

    79 \chardef\isacharbrackright=`\]

    80 \chardef\isacharcircum=`\^

    81 \chardef\isacharunderscore=`\_

    82 \chardef\isacharbackquote=`\`

    83 \chardef\isacharbraceleft=`\{

    84 \chardef\isacharbar=`\|

    85 \chardef\isacharbraceright=`\}

    86 \chardef\isachartilde=`\~

    89 % keyword and section markup

    91 \newcommand{\isakeywordcharunderscore}{\_}

    92 \newcommand{\isakeyword}[1]

    93 {\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%

    94 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}

    95 \newcommand{\isacommand}[1]{\isakeyword{#1}}

    97 \newcommand{\isamarkupheader}[1]{\section{#1}}

    98 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}

    99 \newcommand{\isamarkupsection}[1]{\section{#1}}

   100 \newcommand{\isamarkupsubsection}[1]{\subsection{#1}}

   101 \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}

   102 \newcommand{\isamarkupsect}[1]{\section{#1}}

   103 \newcommand{\isamarkupsubsect}[1]{\subsection{#1}}

   104 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}

   106 \newif\ifisamarkup

   107 \newcommand{\isabeginpar}{\par\ifisamarkup\relax\else\medskip\fi}

   108 \newcommand{\isaendpar}{\par\medskip}

   109 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}

   110 \newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}

   111 \newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}

   112 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}

   115 % alternative styles

   117 \newcommand{\isabellestyle}{}

   118 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}

   120 \newcommand{\isabellestylett}{%

   121 \renewcommand{\isastyle}{\small\tt}%

   122 \renewcommand{\isastyleminor}{\small\tt}%

   123 \renewcommand{\isastylescript}{\footnotesize\tt}%

   124 }

   125 \newcommand{\isabellestyleit}{%

   126 \renewcommand{\isastyle}{\small\it}%

   127 \renewcommand{\isastyleminor}{\it}%

   128 \renewcommand{\isastylescript}{\footnotesize\it}%

   129 \renewcommand{\isakeywordcharunderscore}{\mbox{-}}%

   130 \renewcommand{\isacharbang}{\isamath{!}}%

   131 \renewcommand{\isachardoublequote}{}%

   132 \renewcommand{\isacharhash}{\isamath{\#}}%

   133 \renewcommand{\isachardollar}{\isamath{\$}}%

   134 \renewcommand{\isacharpercent}{\isamath{\%}}%

   135 \renewcommand{\isacharampersand}{\isamath{\&}}%

   136 \renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%

   137 \renewcommand{\isacharparenleft}{\isamath{(}}%

   138 \renewcommand{\isacharparenright}{\isamath{)}}%

   139 \renewcommand{\isacharasterisk}{\isamath{*}}%

   140 \renewcommand{\isacharplus}{\isamath{+}}%

   141 \renewcommand{\isacharcomma}{\isamath{\mathord,}}%

   142 \renewcommand{\isacharminus}{\isamath{-}}%

   143 \renewcommand{\isachardot}{\isamath{\mathord.}}%

   144 \renewcommand{\isacharslash}{\isamath{/}}%

   145 \renewcommand{\isacharcolon}{\isamath{\mathord:}}%

   146 \renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%

   147 \renewcommand{\isacharless}{\isamath{<}}%

   148 \renewcommand{\isacharequal}{\isamath{=}}%

   149 \renewcommand{\isachargreater}{\isamath{>}}%

   150 \renewcommand{\isacharat}{\isamath{@}}%

   151 \renewcommand{\isacharbrackleft}{\isamath{[}}%

   152 \renewcommand{\isacharbackslash}{\isamath{\backslash}}%

   153 \renewcommand{\isacharbrackright}{\isamath{]}}%

   154 \renewcommand{\isacharunderscore}{\mbox{-}}%

   155 \renewcommand{\isacharbraceleft}{\isamath{\{}}%

   156 \renewcommand{\isacharbar}{\isamath{\mid}}%

   157 \renewcommand{\isacharbraceright}{\isamath{\}}}%

   158 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%

   159 }

   161 \newcommand{\isabellestylesl}{%

   162 \isabellestyleit%

   163 \renewcommand{\isastyle}{\small\sl}%

   164 \renewcommand{\isastyleminor}{\sl}%

   165 \renewcommand{\isastylescript}{\footnotesize\sl}%

   166 }

   169 % tagged regions

   171 %plain TeX version of comment package -- much faster!

   172 \let\isafmtname\fmtname\def\fmtname{plain}

   173 \usepackage{comment}

   174 \let\fmtname\isafmtname

   176 \newcommand{\isafold}[1]{\emph{$\langle\mathord{\mathit{#1}}\rangle$}}

   178 \newcommand{\isakeeptag}[1]%

   179 {\includecomment{isadelim#1}\includecomment{isatag#1}\csarg\def{isafold#1}{}}

   180 \newcommand{\isadroptag}[1]%

   181 {\excludecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{}}

   182 \newcommand{\isafoldtag}[1]%

   183 {\includecomment{isadelim#1}\excludecomment{isatag#1}\csarg\def{isafold#1}{\isafold{#1}}}

   185 \isakeeptag{theory}

   186 \isakeeptag{proof}

   187 \isakeeptag{ML}

   188 \isakeeptag{visible}

   189 \isadroptag{invisible}

   191 \IfFileExists{isabelletags.sty}{\usepackage{isabelletags}}{}

author	wenzelm
	Tue, 16 Aug 2005 13:42:18 +0200
changeset 17052	30781cc78fc6
parent 16558	e97188c6bd71
child 17158	d68bf267cbba
permissions	-rw-r--r--