tuned printing of _ in latex
authornipkow
Fri, 28 Sep 2012 08:09:28 +0200
changeset 5064234ada66545ca
parent 50641 354f35953800
child 50643 8262d35eff20
tuned printing of _ in latex
src/Doc/ProgProve/document/prelude.tex
     1.1 --- a/src/Doc/ProgProve/document/prelude.tex	Thu Sep 27 20:30:32 2012 +0200
     1.2 +++ b/src/Doc/ProgProve/document/prelude.tex	Fri Sep 28 08:09:28 2012 +0200
     1.3 @@ -57,12 +57,13 @@
     1.4  \renewcommand{\isamarkupsubsection}[1]{{\rmfamily\subsubsection{#1}}}
     1.5  % isabelle in-text command font
     1.6  \newcommand{\isacom}[1]{\isa{\isacommand{#1}}}
     1.7 +
     1.8 +\protected\def\isacharunderscore{\raisebox{2pt}{\_\kern-1.7pt}}
     1.9 +\protected\def\isacharunderscorekeyword{\raisebox{2pt}{\_}}
    1.10  % isabelle keyword, adapted from isabelle.sty
    1.11  \renewcommand{\isakeyword}[1]
    1.12 -{\emph{\def\isachardot{.}%
    1.13 +{\emph{\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
    1.14  \def\isacharbraceleft{\{}\def\isacharbraceright{\}}\textbf{#1}}}
    1.15 -\renewcommand{\isacharunderscore}{\_}
    1.16 -\renewcommand{\isacharunderscorekeyword}{\_}
    1.17  
    1.18  % add \noindent to text blocks automatically
    1.19  \renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}