lib/texinputs/isabelle.sty
author wenzelm
Fri Mar 17 17:10:37 2000 +0100 (2000-03-17)
changeset 8501 2ff3d25943f1
parent 8489 bb41d88f7df5
child 8512 9c5edbf5eefd
permissions -rw-r--r--
\isamarkupheader: \section;
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@7788
     9
% basic environment
wenzelm@7788
    10
wenzelm@8474
    11
\newcommand{\isabellestyle}{}
wenzelm@8474
    12
\newenvironment{isabelle}{%
wenzelm@8489
    13
\newdimen\@parindent\@parindent\parindent\parindent0pt%
wenzelm@8489
    14
\newdimen\@parskip\@parskip\parskip\parskip0.5ex%
wenzelm@8474
    15
\small\tt\slshape\isabellestyle\mbox{}}{}
wenzelm@7709
    16
\newcommand{\isanewline}{\mbox{}\\\mbox{}}
wenzelm@7752
    17
wenzelm@7797
    18
\chardef\isabraceleft=`\{
wenzelm@7797
    19
\chardef\isabraceright=`\}
wenzelm@7797
    20
\chardef\isatilde=`\~
wenzelm@7797
    21
\chardef\isacircum=`\^
wenzelm@7797
    22
\chardef\isabackslash=`\\
wenzelm@7788
    23
wenzelm@7797
    24
wenzelm@7797
    25
% keyword and section markup
wenzelm@7788
    26
wenzelm@7918
    27
\newcommand{\isacommand}[1]{\emph{\bf #1}}
wenzelm@7918
    28
\newcommand{\isakeyword}[1]{\emph{\bf #1}}
wenzelm@7797
    29
\newcommand{\isabeginblock}{\isakeyword{\{}}
wenzelm@7797
    30
\newcommand{\isaendblock}{\isakeyword{\}}}
wenzelm@7758
    31
wenzelm@8474
    32
\newcommand{\isapar}[1]{%
wenzelm@8489
    33
{\parindent\@parindent\parskip\@parskip\par\medskip #1}\par\smallskip}
wenzelm@8501
    34
\newcommand{\isamarkupheader}[1]{\section{#1}}
wenzelm@7758
    35
wenzelm@7752
    36
\newcommand{\isamarkupchapter}[1]{\chapter{#1}}
wenzelm@7752
    37
\newcommand{\isamarkupsection}[1]{\section{#1}}
wenzelm@7752
    38
\newcommand{\isamarkupsubsection}[1]{\subsection{#1}}
wenzelm@7752
    39
\newcommand{\isamarkupsubsubsection}[1]{\subsubsection{#1}}
wenzelm@7758
    40
\newcommand{\isamarkuptext}[1]{\isapar{\normalsize\rm #1}}
wenzelm@7752
    41
wenzelm@7752
    42
\newcommand{\isamarkupsect}[1]{\section{#1}}
wenzelm@7752
    43
\newcommand{\isamarkupsubsect}[1]{\subsection{#1}}
wenzelm@7752
    44
\newcommand{\isamarkupsubsubsect}[1]{\subsubsection{#1}}
wenzelm@7758
    45
\newcommand{\isamarkuptxt}[1]{\isapar{\rm #1}}
wenzelm@7758
    46
\newcommand{\isamarkupcmt}[1]{{\rm--- #1}}