doc-src/IsarAdvanced/Codegen/style.sty
changeset 30228 2aaf339fb7c1
parent 30224 79136ce06bdb
parent 30227 853abb4853cc
child 30229 9861257b18e6
child 30243 09d5944e224e
equal deleted inserted replaced
30224:79136ce06bdb 30228:2aaf339fb7c1
     1 
       
     2 %% toc
       
     3 \newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
       
     4 \@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}
       
     5 
       
     6 %% references
       
     7 \newcommand{\secref}[1]{\S\ref{#1}}
       
     8 
       
     9 %% logical markup
       
    10 \newcommand{\strong}[1]{{\bfseries {#1}}}
       
    11 \newcommand{\qn}[1]{\emph{#1}}
       
    12 
       
    13 %% typographic conventions
       
    14 \newcommand{\qt}[1]{``{#1}''}
       
    15 
       
    16 %% verbatim text
       
    17 \newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}
       
    18 
       
    19 %% quoted segments
       
    20 \makeatletter
       
    21 \isakeeptag{quote}
       
    22 \newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
       
    23 \renewcommand{\isatagquote}{\begin{quotesegment}}
       
    24 \renewcommand{\endisatagquote}{\end{quotesegment}}
       
    25 \makeatother
       
    26 
       
    27 \isakeeptag{quotett}
       
    28 \renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle}
       
    29 \renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle}
       
    30 
       
    31 %% a trick
       
    32 \newcommand{\isasymSML}{SML}
       
    33 
       
    34 %% presentation
       
    35 \setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
       
    36 
       
    37 \pagestyle{headings}
       
    38 \binperiod
       
    39 \underscoreoff
       
    40 
       
    41 \renewcommand{\isadigit}[1]{\isamath{#1}}
       
    42 
       
    43 %% ml reference
       
    44 \newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
       
    45 
       
    46 \isakeeptag{mlref}
       
    47 \renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
       
    48 \renewcommand{\endisatagmlref}{\endgroup}
       
    49 
       
    50 \isabellestyle{it}
       
    51 
       
    52 
       
    53 %%% Local Variables: 
       
    54 %%% mode: latex
       
    55 %%% TeX-master: "implementation"
       
    56 %%% End: