# HG changeset patch
# User wenzelm
# Date 973359749 -3600
# Node ID b2a212304fb4193c1eed76dbdd531e62047e9350
# Parent  f27afee8475da9fe944cd2e9ebe5e5ab5b7e4464
isamarkup: handle % in input;

diff -r f27afee8475d -r b2a212304fb4 src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Sat Nov 04 18:41:37 2000 +0100
+++ b/src/Pure/Thy/latex.ML	Sat Nov 04 18:42:29 2000 +0100
@@ -107,7 +107,7 @@
         else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
         else output_syms s
       end
-  | output_tok (Markup cmd, txt) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
+  | output_tok (Markup cmd, txt) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "%\n}\n"
   | output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
       strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
   | output_tok (Verbatim, txt) = "%\n" ^ strip_blanks txt ^ "\n";