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