# HG changeset patch
# User nipkow
# Date 1348812568 -7200
# Node ID 34ada66545ca27885897b7edaef165f62751f18a
# Parent  354f359538004a4426ae20d5bed729861bd19195
tuned printing of _ in latex

diff -r 354f35953800 -r 34ada66545ca src/Doc/ProgProve/document/prelude.tex
--- a/src/Doc/ProgProve/document/prelude.tex	Thu Sep 27 20:30:32 2012 +0200
+++ b/src/Doc/ProgProve/document/prelude.tex	Fri Sep 28 08:09:28 2012 +0200
@@ -57,12 +57,13 @@
 \renewcommand{\isamarkupsubsection}[1]{{\rmfamily\subsubsection{#1}}}
 % isabelle in-text command font
 \newcommand{\isacom}[1]{\isa{\isacommand{#1}}}
+
+\protected\def\isacharunderscore{\raisebox{2pt}{\_\kern-1.7pt}}
+\protected\def\isacharunderscorekeyword{\raisebox{2pt}{\_}}
 % isabelle keyword, adapted from isabelle.sty
 \renewcommand{\isakeyword}[1]
-{\emph{\def\isachardot{.}%
+{\emph{\def\isachardot{.}\def\isacharunderscore{\isacharunderscorekeyword}%
 \def\isacharbraceleft{\{}\def\isacharbraceright{\}}\textbf{#1}}}
-\renewcommand{\isacharunderscore}{\_}
-\renewcommand{\isacharunderscorekeyword}{\_}
 
 % add \noindent to text blocks automatically
 \renewenvironment{isamarkuptext}{\par\isastyletext\begin{isapar}\noindent}{\end{isapar}}