underscore: added \mbox to avoid hyphenation;
authorwenzelm
Tue, 29 Aug 2000 20:10:39 +0200
changeset 9725 d53e4fd36448
parent 9724 2030c5d63741
child 9726 78f9bcd9585e
underscore: added \mbox to avoid hyphenation;
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{$\}$}}%