# HG changeset patch
# User wenzelm
# Date 1209761243 -7200
# Node ID e258050a30764b0f10e2b13cfdac829253e29c95
# Parent  ba8b1a8a12a7919972e5b732e0072cd663d72717
output_entity: added \mbox{} to prevent hyphenation;

diff -r ba8b1a8a12a7 -r e258050a3076 doc-src/antiquote_setup.ML
--- a/doc-src/antiquote_setup.ML	Fri May 02 22:43:14 2008 +0200
+++ b/doc-src/antiquote_setup.ML	Fri May 02 22:47:23 2008 +0200
@@ -150,7 +150,7 @@
     |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
     |> (if ! O.quotes then quote else I)
     |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
-        else enclose "\\isa{" "}"));
+        else enclose "\\mbox{\\isa{" "}}"));
 
 fun entity markup index kind =
   O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))