src/Pure/Thy/latex.ML
changeset 7852 d28dff7ac48d
parent 7800 8ee919e42174
child 7900 e62973fccc97
     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;