doc-src/TutorialI/isabelle.sty
author nipkow
Wed Dec 06 13:22:58 2000 +0100 (2000-12-06)
changeset 10608 620647438780
parent 10589 b2d1b393b750
child 10823 88cb1547d952
permissions -rw-r--r--
*** empty log message ***
     1 %%
     2 %% $Id$
     3 %% Author: Markus Wenzel, TU Muenchen
     4 %% License: GPL (GNU GENERAL PUBLIC LICENSE)
     5 %%
     6 %% macros for Isabelle generated LaTeX output
     7 %%
     8 
     9 %%% Simple document preparation (based on theory token language and symbols)
    10 
    11 % isabelle environments
    12 
    13 \newcommand{\isabellecontext}{UNKNOWN}
    14 
    15 \newcommand{\isastyle}{\small\tt\slshape}
    16 \newcommand{\isastyleminor}{\small\tt\slshape}
    17 \newcommand{\isastylescript}{\footnotesize\tt\slshape}
    18 \newcommand{\isastyletext}{\normalsize\rm}
    19 \newcommand{\isastyletxt}{\rm}
    20 \newcommand{\isastylecmt}{\rm}
    21 
    22 %symbol markup -- \emph achieves decent spacing via italic corrections
    23 \newcommand{\isamath}[1]{\emph{$#1$}}
    24 \newcommand{\isatext}[1]{\emph{#1}}
    25 \newcommand{\isascriptstyle}{\def\isamath##1{##1}\def\isatext##1{\mbox{\isastylescript##1}}}
    26 \newcommand{\isactrlsub}[1]{\emph{\isascriptstyle${}\sb{#1}$}}
    27 \newcommand{\isactrlsup}[1]{\emph{\isascriptstyle${}\sp{#1}$}}
    28 
    29 \newdimen\isa@parindent\newdimen\isa@parskip
    30 
    31 \newenvironment{isabellebody}{%
    32 \par%
    33 \isa@parindent\parindent\parindent0pt%
    34 \isa@parskip\parskip\parskip0pt%
    35 \isastyle}{\par}
    36 
    37 \newenvironment{isabelle}
    38 {\begin{trivlist}\begin{isabellebody}\item\relax}
    39 {\end{isabellebody}\end{trivlist}}
    40 
    41 \newcommand{\isa}[1]{\emph{\isastyleminor #1}}
    42 
    43 \newcommand{\isanewline}{\mbox{}\\\mbox{}}
    44 \newcommand{\isadigit}[1]{#1}
    45 
    46 \chardef\isacharbang=`\!
    47 \chardef\isachardoublequote=`\"
    48 \chardef\isacharhash=`\#
    49 \chardef\isachardollar=`\$
    50 \chardef\isacharpercent=`\%
    51 \chardef\isacharampersand=`\&
    52 \chardef\isacharprime=`\'
    53 \chardef\isacharparenleft=`\(
    54 \chardef\isacharparenright=`\)
    55 \chardef\isacharasterisk=`\*
    56 \chardef\isacharplus=`\+
    57 \chardef\isacharcomma=`\,
    58 \chardef\isacharminus=`\-
    59 \chardef\isachardot=`\.
    60 \chardef\isacharslash=`\/
    61 \chardef\isacharcolon=`\:
    62 \chardef\isacharsemicolon=`\;
    63 \chardef\isacharless=`\<
    64 \chardef\isacharequal=`\=
    65 \chardef\isachargreater=`\>
    66 \chardef\isacharquery=`\?
    67 \chardef\isacharat=`\@
    68 \chardef\isacharbrackleft=`\[
    69 \chardef\isacharbackslash=`\\
    70 \chardef\isacharbrackright=`\]
    71 \chardef\isacharcircum=`\^
    72 \chardef\isacharunderscore=`\_
    73 \chardef\isacharbackquote=`\`
    74 \chardef\isacharbraceleft=`\{
    75 \chardef\isacharbar=`\|
    76 \chardef\isacharbraceright=`\}
    77 \chardef\isachartilde=`\~
    78 
    79 
    80 % keyword and section markup
    81 
    82 \newcommand{\isakeywordcharunderscore}{\_}
    83 \newcommand{\isakeyword}[1]
    84 {\emph{\bf\def\isachardot{.}\def\isacharunderscore{\isakeywordcharunderscore}%
    85 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}#1}}
    86 \newcommand{\isacommand}[1]{\isakeyword{#1}}
    87 
    88 \newcommand{\isamarkupheader}[1]{\section{#1}}
    89 \newcommand{\isamarkupchapter}[1]{\chapter{#1}}
    90 \newcommand{\isamarkupsection}[1]{\section{#1}}
    91 \newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
    92 \newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
    93 \newcommand{\isamarkupsect}[1]{\section{#1}}
    94 \newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
    95 \newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
    96 
    97 \newcommand{\isabeginpar}{\par\medskip}
    98 \newcommand{\isaendpar}{\par\medskip}
    99 \newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\isabeginpar}{\isaendpar}
   100 \newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
   101 \newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
   102 \newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
   103 
   104 
   105 % alternative styles
   106 
   107 \newcommand{\isabellestyle}{}
   108 \def\isabellestyle#1{\csname isabellestyle#1\endcsname}
   109 
   110 \newcommand{\isabellestylett}{%
   111 \renewcommand{\isastyle}{\small\tt}%
   112 \renewcommand{\isastyleminor}{\small\tt}%
   113 \renewcommand{\isastylescript}{\footnotesize\tt}%
   114 }
   115 \newcommand{\isabellestyleit}{%
   116 \renewcommand{\isastyle}{\small\it}%
   117 \renewcommand{\isastyleminor}{\it}%
   118 \renewcommand{\isastylescript}{\footnotesize\it}%
   119 \renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
   120 \renewcommand{\isacharbang}{\isamath{!}}%
   121 \renewcommand{\isachardoublequote}{}%
   122 \renewcommand{\isacharhash}{\isamath{\#}}%
   123 \renewcommand{\isachardollar}{\isamath{\$}}%
   124 \renewcommand{\isacharpercent}{\isamath{\%}}%
   125 \renewcommand{\isacharampersand}{\isamath{\&}}%
   126 \renewcommand{\isacharprime}{\isamath{\mskip2mu{'}\mskip-2mu}}%
   127 \renewcommand{\isacharparenleft}{\isamath{(}}%
   128 \renewcommand{\isacharparenright}{\isamath{)}}%
   129 \renewcommand{\isacharasterisk}{\isamath{*}}%
   130 \renewcommand{\isacharplus}{\isamath{+}}%
   131 \renewcommand{\isacharcomma}{\isamath{\mathord,}}%
   132 \renewcommand{\isacharminus}{\isamath{-}}%
   133 \renewcommand{\isachardot}{\isamath{\mathord.}}%
   134 \renewcommand{\isacharslash}{\isamath{/}}%
   135 \renewcommand{\isacharcolon}{\isamath{\mathord:}}%
   136 \renewcommand{\isacharsemicolon}{\isamath{\mathord;}}%
   137 \renewcommand{\isacharless}{\isamath{<}}%
   138 \renewcommand{\isacharequal}{\isamath{=}}%
   139 \renewcommand{\isachargreater}{\isamath{>}}%
   140 \renewcommand{\isacharat}{\isamath{@}}%
   141 \renewcommand{\isacharbrackleft}{\isamath{[}}%
   142 \renewcommand{\isacharbrackright}{\isamath{]}}%
   143 \renewcommand{\isacharunderscore}{\mbox{-}}%
   144 \renewcommand{\isacharbraceleft}{\isamath{\{}}%
   145 \renewcommand{\isacharbar}{\isamath{\mid}}%
   146 \renewcommand{\isacharbraceright}{\isamath{\}}}%
   147 \renewcommand{\isachartilde}{\isamath{{}\sp{\sim}}}%
   148 }
   149 
   150 \newcommand{\isabellestylesl}{%
   151 \isabellestyleit%
   152 \renewcommand{\isastyle}{\small\sl}%
   153 \renewcommand{\isastyleminor}{\sl}%
   154 \renewcommand{\isastylescript}{\footnotesize\sl}%
   155 }