ensure separation of TeX tokens;
authorwenzelm
Tue Dec 12 17:47:00 2017 +0100 (17 months ago)
changeset 67189725897bbabef
parent 67188 bc7a6455e12a
child 67190 58ab7ddbdb04
ensure separation of TeX tokens;
src/Pure/Thy/latex.ML
     1.1 --- a/src/Pure/Thy/latex.ML	Tue Dec 12 16:12:48 2017 +0100
     1.2 +++ b/src/Pure/Thy/latex.ML	Tue Dec 12 17:47:00 2017 +0100
     1.3 @@ -189,7 +189,7 @@
     1.4        (case take_prefix is_blank_line (split_lines output) of
     1.5          (_, []) => output
     1.6        | (blank, rest) =>
     1.7 -          cat_lines blank ^ "%\n" ^
     1.8 +          cat_lines blank ^ " %\n" ^
     1.9            output_prop (Markup.lineN, Value.print_int n) ^
    1.10            cat_lines rest));
    1.11