markup / varbatim: comment out (%) newline char;
authorwenzelm
Wed Oct 13 19:41:18 1999 +0200 (1999-10-13)
changeset 7852d28dff7ac48d
parent 7851 4a6df182b093
child 7853 a4acf1b4d5a8
markup / varbatim: comment out (%) newline char;
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Wed Oct 13 19:40:23 1999 +0200
     1.2 +++ b/src/Pure/Thy/latex.ML	Wed Oct 13 19:41:18 1999 +0200
     1.3 @@ -64,8 +64,8 @@
     1.4          else if T.is_kind T.Verbatim tok then output_sym (enclose "{*" "*}" s)
     1.5          else output_sym s
     1.6        end
     1.7 -  | output_tok (Markup (cmd, txt)) = "\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
     1.8 -  | output_tok (Verbatim txt) = "\n" ^ strip_blanks txt ^ "\n";
     1.9 +  | output_tok (Markup (cmd, txt)) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
    1.10 +  | output_tok (Verbatim txt) = "%\n" ^ strip_blanks txt ^ "\n";
    1.11  
    1.12  
    1.13  val output_tokens = implode o map output_tok;