output_entity: added \mbox{} to prevent hyphenation;
authorwenzelm
Fri May 02 22:47:23 2008 +0200 (2008-05-02)
changeset 26774e258050a3076
parent 26773 ba8b1a8a12a7
child 26775 06d6b1242dcf
output_entity: added \mbox{} to prevent hyphenation;
doc-src/antiquote_setup.ML
     1.1 --- a/doc-src/antiquote_setup.ML	Fri May 02 22:43:14 2008 +0200
     1.2 +++ b/doc-src/antiquote_setup.ML	Fri May 02 22:47:23 2008 +0200
     1.3 @@ -150,7 +150,7 @@
     1.4      |> (if markup = "" then I else enclose ("\\" ^ markup ^ "{") "}")
     1.5      |> (if ! O.quotes then quote else I)
     1.6      |> (if ! O.display then enclose "\\begin{isabelle}%\n" "%\n\\end{isabelle}"
     1.7 -        else enclose "\\isa{" "}"));
     1.8 +        else enclose "\\mbox{\\isa{" "}}"));
     1.9  
    1.10  fun entity markup index kind =
    1.11    O.args (Scan.lift (Scan.optional (Args.parens Args.name) "" -- Args.name))