doc-src/IsarAdvanced/Codegen/style.sty

\underscoreoff is now default

%% toc
\newcommand{\tocentry}[1]{\cleardoublepage\phantomsection\addcontentsline{toc}{chapter}{#1}
\@mkboth{\MakeUppercase{#1}}{\MakeUppercase{#1}}}

%% references
\newcommand{\secref}[1]{\S\ref{#1}}

%% index
\newcommand{\indexml}[1]{\index{\emph{#1}|bold}}
\newcommand{\indexmltype}[1]{\index{\emph{#1} (type)|bold}}
\newcommand{\indexmlstructure}[1]{\index{\emph{#1} (structure)|bold}}
\newcommand{\indexmlfunctor}[1]{\index{\emph{#1} (functor)|bold}}

%% logical markup
\newcommand{\strong}[1]{{\bfseries {#1}}}
\newcommand{\qn}[1]{\emph{#1}}

%% typographic conventions
\newcommand{\qt}[1]{``{#1}''}

%% verbatim text
\newcommand{\isatypewriter}{\fontsize{9pt}{0pt}\tt\renewcommand{\baselinestretch}{1}\setlength{\baselineskip}{9pt}}

%% quoted segments
\makeatletter
\isakeeptag{quote}
\newenvironment{quotesegment}{\begin{quote}\isa@parindent\parindent\parindent0pt\isa@parskip\parskip\parskip0pt}{\end{quote}}
\renewcommand{\isatagquote}{\begin{quotesegment}}
\renewcommand{\endisatagquote}{\end{quotesegment}}
\makeatother

\isakeeptag{quotett}
\renewcommand{\isatagquotett}{\begin{quotesegment}\isabellestyle{tt}\isastyle}
\renewcommand{\endisatagquotett}{\end{quotesegment}\isabellestyle{it}\isastyle}

%% a trick
\newcommand{\isasymSML}{SML}

%% presentation
\setcounter{secnumdepth}{2} \setcounter{tocdepth}{2}

\pagestyle{headings}
\binperiod
\underscoreoff

\renewcommand{\isadigit}[1]{\isamath{#1}}

%% ml reference
\newenvironment{mldecls}{\par\noindent\begingroup\footnotesize\def\isanewline{\\}\begin{tabular}{l}}{\end{tabular}\smallskip\endgroup}

\isakeeptag{mlref}
\renewcommand{\isatagmlref}{\subsection*{\makebox[0pt][r]{\fbox{\ML}~~}Reference}\begingroup\def\isastyletext{\rm}\small}
\renewcommand{\endisatagmlref}{\endgroup}

\isabellestyle{it}


%%% Local Variables: 
%%% mode: latex
%%% TeX-master: "implementation"
%%% End: