lib/texinputs/isabelle.sty
author wenzelm
Sat Aug 19 12:43:55 2000 +0200 (2000-08-19)
changeset 9657 0a187a43ef21
parent 8822 ea36d70ff7d3
child 9669 542fb6c6c9b2
permissions -rw-r--r--
added \isachar definitions;
added \isabellestyle switch;
tuned;
wenzelm@7709
     1
%%
wenzelm@7709
     2
%% $Id$
wenzelm@7709
     3
%%
wenzelm@7709
     4
%% macros for Isabelle generated LaTeX output
wenzelm@7709
     5
%%
wenzelm@7709
     6
wenzelm@7709
     7
%%% Simple document preparation (based on theory token language)
wenzelm@7709
     8
wenzelm@8714
     9
% isabelle environments
wenzelm@7788
    10
wenzelm@9657
    11
\newcommand{\isastyle}{\small\tt\slshape}
wenzelm@9657
    12
\newcommand{\isastyletext}{\normalsize\rm}
wenzelm@9657
    13
\newcommand{\isastyletxt}{\rm}
wenzelm@9657
    14
\newcommand{\isastylecmt}{\rm}
wenzelm@8713
    15
wenzelm@8713
    16
\newdimen\isa@parindent\newdimen\isa@parskip
wenzelm@9657
    17
wenzelm@8474
    18
\newenvironment{isabelle}{%
wenzelm@8713
    19
\isa@parindent\parindent\parindent0pt%
wenzelm@8713
    20
\isa@parskip\parskip\parskip0pt%
wenzelm@9657
    21
\isastyle}{}
wenzelm@8713
    22
wenzelm@9657
    23
\newcommand{\isa}[1]{\emph{\isastyle #1}}
wenzelm@8714
    24
wenzelm@7709
    25
\newcommand{\isanewline}{\mbox{}\\\mbox{}}
wenzelm@7752
    26
wenzelm@9657
    27
\chardef\isacharhash=`\#
wenzelm@9657
    28
\chardef\isachardollar=`\$
wenzelm@9657
    29
\chardef\isacharpercent=`\%
wenzelm@9657
    30
\chardef\isacharampersand=`\&
wenzelm@9657
    31
\chardef\isacharprime=`\'
wenzelm@9657
    32
\chardef\isacharparenleft=`\(
wenzelm@9657
    33
\chardef\isacharparenright=`\)
wenzelm@9657
    34
\chardef\isacharasterisk=`\*
wenzelm@9657
    35
\chardef\isacharminus=`\-
wenzelm@9657
    36
\chardef\isacharless=`\<
wenzelm@9657
    37
\chardef\isachargreater=`\>
wenzelm@9657
    38
\chardef\isacharbrackleft=`\[
wenzelm@9657
    39
\chardef\isachardoublequote=`\"
wenzelm@9657
    40
\chardef\isacharbackslash=`\\
wenzelm@9657
    41
\chardef\isacharbrackright=`\]
wenzelm@9657
    42
\chardef\isacharcircum=`\^
wenzelm@9657
    43
\chardef\isacharunderscore=`\_
wenzelm@9657
    44
\chardef\isacharbraceleft=`\{
wenzelm@9657
    45
\chardef\isacharbar=`\|
wenzelm@9657
    46
\chardef\isacharbraceright=`\}
wenzelm@9657
    47
\chardef\isachartilde=`\~
wenzelm@7788
    48
wenzelm@7797
    49
wenzelm@7797
    50
% keyword and section markup
wenzelm@7788
    51
wenzelm@7918
    52
\newcommand{\isacommand}[1]{\emph{\bf #1}}
wenzelm@7918
    53
\newcommand{\isakeyword}[1]{\emph{\bf #1}}
wenzelm@7797
    54
\newcommand{\isabeginblock}{\isakeyword{\{}}
wenzelm@7797
    55
\newcommand{\isaendblock}{\isakeyword{\}}}
wenzelm@7758
    56
wenzelm@8501
    57
\newcommand{\isamarkupheader}[1]{\section{#1}}
wenzelm@7752
    58
\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
wenzelm@7752
    59
\newcommand{\isamarkupsection}[1]{\section{#1}}
wenzelm@7752
    60
\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
wenzelm@7752
    61
\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
wenzelm@7752
    62
\newcommand{\isamarkupsect}[1]{\section{#1}}
wenzelm@7752
    63
\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
wenzelm@7752
    64
\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
wenzelm@8662
    65
wenzelm@8713
    66
\newenvironment{isapar}{\parindent\isa@parindent\parskip\isa@parskip\par\medskip}{\par\smallskip}
wenzelm@9657
    67
\newenvironment{isamarkuptext}{\isastyletext\begin{isapar}}{\end{isapar}}
wenzelm@9657
    68
\newenvironment{isamarkuptxt}{\isastyletxt\begin{isapar}}{\end{isapar}}
wenzelm@9657
    69
\newcommand{\isamarkupcmt}[1]{{\isastylecmt--- #1}}
wenzelm@9657
    70
wenzelm@9657
    71
wenzelm@9657
    72
% alternative styles -- default is "tt"
wenzelm@9657
    73
wenzelm@9657
    74
\newcommand{\isabellestyle}{}
wenzelm@9657
    75
\def\isabellestyle#1{\csname isasetup#1\endcsname}
wenzelm@9657
    76
wenzelm@9657
    77
\newcommand{\isasetupit}{%
wenzelm@9657
    78
\renewcommand{\isastyle}{\small\itshape}%
wenzelm@9657
    79
\renewcommand{\isastyletext}{\normalsize\rm}%
wenzelm@9657
    80
\renewcommand{\isastyletxt}{\rm}%
wenzelm@9657
    81
\renewcommand{\isastylecmt}{\rm}%
wenzelm@9657
    82
\renewcommand{\isachardollar}{\textsl{\$}}%
wenzelm@9657
    83
\renewcommand{\isacharampersand}{\textsl{\&}}%
wenzelm@9657
    84
\renewcommand{\isacharprime}{$'$}%
wenzelm@9657
    85
\renewcommand{\isacharparenleft}{\emph{$($}}%
wenzelm@9657
    86
\renewcommand{\isacharparenright}{\emph{$)$}}%
wenzelm@9657
    87
\renewcommand{\isacharasterisk}{\emph{$*$}}%
wenzelm@9657
    88
\renewcommand{\isacharminus}{\emph{$-$}}%
wenzelm@9657
    89
\renewcommand{\isacharless}{\emph{$<$}}%
wenzelm@9657
    90
\renewcommand{\isachargreater}{\emph{$>$}}%
wenzelm@9657
    91
\renewcommand{\isachardoublequote}{}%
wenzelm@9657
    92
\renewcommand{\isacharbrackleft}{\emph{$[$}}%
wenzelm@9657
    93
\renewcommand{\isacharbrackright}{\emph{$]$}}%
wenzelm@9657
    94
\renewcommand{\isacharunderscore}{-}%
wenzelm@9657
    95
\renewcommand{\isacharbraceleft}{\emph{$\{$}}%
wenzelm@9657
    96
\renewcommand{\isacharbar}{\emph{$\mid$}}%
wenzelm@9657
    97
\renewcommand{\isacharbraceright}{\emph{$\}$}}%
wenzelm@9657
    98
}
wenzelm@9657
    99
wenzelm@9657
   100
\newcommand{\isasetupsl}{\isasetupit\renewcommand{\isastyle}{\small\slshape}}
wenzelm@9657
   101