# HG changeset patch
# User wenzelm
# Date 967572639 -7200
# Node ID d53e4fd364488808241048b5daf466d3ae393f64
# Parent  2030c5d6374189f7747d2c333d8d3baf1eb4fbbc
underscore: added \mbox to avoid hyphenation;

diff -r 2030c5d63741 -r d53e4fd36448 lib/texinputs/isabelle.sty
--- a/lib/texinputs/isabelle.sty	Tue Aug 29 20:10:02 2000 +0200
+++ b/lib/texinputs/isabelle.sty	Tue Aug 29 20:10:39 2000 +0200
@@ -95,8 +95,7 @@
 \newcommand{\isabellestyleit}{%
 \renewcommand{\isastyle}{\small\it}%
 \renewcommand{\isastyleminor}{\it}%
-\renewcommand{\isakeywordcharunderscore}{-}%
-%\renewcommand{\isadigit}[1]{\emph{$##1$}}
+\renewcommand{\isakeywordcharunderscore}{\mbox{-}}%
 \renewcommand{\isacharbang}{\emph{$!$}}%
 \renewcommand{\isachardoublequote}{}%
 \renewcommand{\isacharhash}{\emph{$\#$}}%
@@ -117,11 +116,10 @@
 \renewcommand{\isacharless}{\emph{$<$}}%
 \renewcommand{\isacharequal}{\emph{$=$}}%
 \renewcommand{\isachargreater}{\emph{$>$}}%
-%\renewcommand{\isacharquery}{\emph{$\mathord?$}}%
 \renewcommand{\isacharat}{\emph{$@$}}%
 \renewcommand{\isacharbrackleft}{\emph{$[$}}%
 \renewcommand{\isacharbrackright}{\emph{$]$}}%
-\renewcommand{\isacharunderscore}{-}%
+\renewcommand{\isacharunderscore}{\mbox{-}}%
 \renewcommand{\isacharbraceleft}{\emph{$\{$}}%
 \renewcommand{\isacharbar}{\emph{$\mid$}}%
 \renewcommand{\isacharbraceright}{\emph{$\}$}}%