src/Pure/Thy/latex.ML
changeset 10393 b2a212304fb4
parent 10247 33e542b4934c
child 10955 36741b4fe109
     1.1 --- a/src/Pure/Thy/latex.ML	Sat Nov 04 18:41:37 2000 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Sat Nov 04 18:42:29 2000 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4          else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
     1.5          else output_syms s
     1.6        end
     1.7 -  | output_tok (Markup cmd, txt) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
     1.8 +  | output_tok (Markup cmd, txt) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "%\n}\n"
     1.9    | output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
    1.10        strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
    1.11    | output_tok (Verbatim, txt) = "%\n" ^ strip_blanks txt ^ "\n";