doc-src/IsarAdvanced/Codegen/style.sty
author haftmann
Mon Dec 08 10:27:40 2008 +0100 (2008-12-08)
changeset 29017 9a1eaad4a7bb
parent 26781 861e06a047c5
child 29104 a5ac0bc68e2b
permissions -rw-r--r--
tuned LaTeX files
haftmann@20948
     1
haftmann@20948
     2
%% toc
haftmann@20948
     3
\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
haftmann@20948
     4
\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
haftmann@20948
     5
haftmann@20948
     6
%% references
haftmann@20948
     7
\newcommand{\secref}[1]{\S\ref{#1}}
haftmann@20948
     8
haftmann@20948
     9
%% index
haftmann@20948
    10
\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
haftmann@20948
    11
\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
haftmann@20948
    12
\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
haftmann@20948
    13
\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}
haftmann@20948
    14
haftmann@29017
    15
%% logical markup
haftmann@29017
    16
\newcommand{\strong}[1]{{\bfseries {#1}}}
haftmann@29017
    17
\newcommand{\qn}[1]{\emph{#1}}
haftmann@29017
    18
haftmann@29017
    19
%% typographic conventions
haftmann@29017
    20
\newcommand{\qt}[1]{``{#1}''}
haftmann@29017
    21
haftmann@29017
    22
%% verbatim text
haftmann@29017
    23
\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
haftmann@20948
    24
haftmann@29017
    25
%% quoted segments
haftmann@29017
    26
\makeatletter
haftmann@29017
    27
\isakeeptag{quote}
haftmann@29017
    28
\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
haftmann@29017
    29
\renewcommand{\isatagquote}{\begin{quotesegment}}
haftmann@29017
    30
\renewcommand{\endisatagquote}{\end{quotesegment}}
haftmann@29017
    31
\makeatother
haftmann@29017
    32
haftmann@29017
    33
\isakeeptag{quotett}
haftmann@29017
    34
\renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle}
haftmann@29017
    35
\renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle}
haftmann@29017
    36
haftmann@29017
    37
%% a trick
haftmann@29017
    38
\newcommand{\isasymSML}{SML}
haftmann@29017
    39
haftmann@29017
    40
%% presentation
haftmann@20948
    41
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
haftmann@20948
    42
haftmann@20948
    43
\pagestyle{headings}
haftmann@20948
    44
\binperiod
haftmann@20948
    45
\underscoreon
haftmann@20948
    46
haftmann@20948
    47
\renewcommand{\isadigit}[1]{\isamath{#1}}
haftmann@20948
    48
haftmann@29017
    49
%% ml reference
haftmann@20948
    50
\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
haftmann@20948
    51
haftmann@20948
    52
\isakeeptag{mlref}
haftmann@20948
    53
\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
haftmann@20948
    54
\renewcommand{\endisatagmlref}{\endgroup}
haftmann@20948
    55
haftmann@29017
    56
\isabellestyle{it}
haftmann@20948
    57
haftmann@20948
    58
haftmann@20948
    59
%%% Local Variables: 
haftmann@20948
    60
%%% mode: latex
haftmann@20948
    61
%%% TeX-master: "implementation"
haftmann@20948
    62
%%% End: