# 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";