--- a/src/Pure/Thy/latex.ML Wed Oct 13 19:40:23 1999 +0200
+++ b/src/Pure/Thy/latex.ML Wed Oct 13 19:41:18 1999 +0200
@@ -64,8 +64,8 @@
else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
else output_sym s
end
- | output_tok (Markup (cmd, txt)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
- | output_tok (Verbatim txt) = "\n" ^ strip_blanks txt ^ "\n";
+ | output_tok (Markup (cmd, txt)) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
+ | output_tok (Verbatim txt) = "%\n" ^ strip_blanks txt ^ "\n";
val output_tokens = implode o map output_tok;