src/Doc/Codegen/document/style.sty
author wenzelm
Fri, 29 Mar 2019 12:24:34 +0100
changeset 70010 499896e3a7b0
parent 69660 2bc2a8599369
permissions -rw-r--r--
clarified style: allow to search PDF for keywords containing "_";
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
30227
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
     6
%% paragraphs
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
     7
\setlength{\parindent}{1em}
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
     8
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
     9
%% references
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    10
\newcommand{\secref}[1]{\S\ref{#1}}
39665
f1622d126e31 more idiomatic handling of latex typewriter type setting
haftmann
parents: 39664
diff changeset
    11
\newcommand{\figref}[1]{figure~\ref{#1}}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    12
29017
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    13
%% logical markup
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    14
\newcommand{\strong}[1]{{\bfseries {#1}}}
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    15
\newcommand{\qn}[1]{\emph{#1}}
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    16
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    17
%% typographic conventions
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    18
\newcommand{\qt}[1]{``{#1}''}
38404
haftmann
parents: 30227
diff changeset
    19
\newcommand{\ditem}[1]{\item[\isastyletext #1]}
29017
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    20
65041
2525e680f94f basic documentation for computations
haftmann
parents: 48985
diff changeset
    21
%% vectors
2525e680f94f basic documentation for computations
haftmann
parents: 48985
diff changeset
    22
\newcommand{\isactrlvec}[1]{\emph{$\overline{#1}$}}
2525e680f94f basic documentation for computations
haftmann
parents: 48985
diff changeset
    23
30227
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
    24
%% quote environment
29017
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    25
\isakeeptag{quote}
30227
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
    26
\renewenvironment{quote}
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
    27
  {\list{}{\leftmargin2em\rightmargin0pt}\parindent0pt\parskip0pt\item\relax}
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
    28
  {\endlist}
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
    29
\renewcommand{\isatagquote}{\begin{quote}}
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
    30
\renewcommand{\endisatagquote}{\end{quote}}
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
    31
\newcommand{\quotebreak}{\\[1.2ex]}
29017
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    32
39664
0afaf89ab591 more canonical type setting of type writer code examples
haftmann
parents: 39538
diff changeset
    33
%% typewriter text
39746
0da00ec1fd31 combine quote and typewriter tag; typewriter considers isa@parindent
haftmann
parents: 39711
diff changeset
    34
\isakeeptag{quotett}
0da00ec1fd31 combine quote and typewriter tag; typewriter considers isa@parindent
haftmann
parents: 39711
diff changeset
    35
\renewcommand{\isatagquotett}{\begin{quote}\isabellestyle{tt}\isastyle}
0da00ec1fd31 combine quote and typewriter tag; typewriter considers isa@parindent
haftmann
parents: 39711
diff changeset
    36
\renewcommand{\endisatagquotett}{\end{quote}}
29017
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    37
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    38
%% a trick
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    39
\newcommand{\isasymSML}{SML}
40351
090dac52cfd7 SMLdummy target
haftmann
parents: 39746
diff changeset
    40
\newcommand{\isasymSMLdummy}{SML}
29017
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    41
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    42
%% presentation
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    43
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    44
30227
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
    45
%% character detail
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
    46
\renewcommand{\isadigit}[1]{\isamath{#1}}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    47
\binperiod
29104
a5ac0bc68e2b \underscoreoff is now default
haftmann
parents: 29017
diff changeset
    48
\underscoreoff
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    49
30227
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
    50
%% format
853abb4853cc tuned manuals
haftmann
parents: 30226
diff changeset
    51
\pagestyle{headings}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    52
29017
9a1eaad4a7bb tuned LaTeX files
haftmann
parents: 26781
diff changeset
    53
%% ml reference
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    54
\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    55
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    56
\isakeeptag{mlref}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    57
\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    58
\renewcommand{\endisatagmlref}{\endgroup}
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    59
70010
499896e3a7b0 clarified style: allow to search PDF for keywords containing "_";
wenzelm
parents: 69660
diff changeset
    60
\isabellestyle{literalunderscore}
69660
2bc2a8599369 canonical operation to typeset generated code makes dedicated environment obsolete
haftmann
parents: 65041
diff changeset
    61
\def\isastylett{\footnotesize\normalfont\ttfamily}
20948
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    62
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    63
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    64
%%% Local Variables: 
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    65
%%% mode: latex
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    66
%%% TeX-master: "implementation"
9b9910b82645 initial draft
haftmann
parents:
diff changeset
    67
%%% End: