Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
markup / varbatim: comment out (%) newline char;
authorwenzelm
Wed, 13 Oct 1999 19:41:18 +0200
changeset 7852 d28dff7ac48d
parent 7851 4a6df182b093
child 7853 a4acf1b4d5a8
markup / varbatim: comment out (%) newline char;
src/Pure/Thy/latex.ML file | annotate | diff | comparison | revisions 
--- 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;
isabelle