isamarkup: handle % in input;
authorwenzelm
Sat Nov 04 18:42:29 2000 +0100 (2000-11-04)
changeset 10393b2a212304fb4
parent 10392 f27afee8475d
child 10394 eef9e422929a
isamarkup: handle % in input;
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Sat Nov 04 18:41:37 2000 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Sat Nov 04 18:42:29 2000 +0100
     1.3 @@ -107,7 +107,7 @@
     1.4          else if T.is_kind T.Verbatim tok then output_syms (enclose "{*" "*}" s)
     1.5          else output_syms s
     1.6        end
     1.7 -  | output_tok (Markup cmd, txt) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "}\n"
     1.8 +  | output_tok (Markup cmd, txt) = "%\n\\isamarkup" ^ cmd ^ "{" ^ strip_blanks txt ^ "%\n}\n"
     1.9    | output_tok (MarkupEnv cmd, txt) = "%\n\\begin{isamarkup" ^ cmd ^ "}%\n" ^
    1.10        strip_blanks txt ^ "%\n\\end{isamarkup" ^ cmd ^ "}%\n"
    1.11    | output_tok (Verbatim, txt) = "%\n" ^ strip_blanks txt ^ "\n";