# HG changeset patch
# User wenzelm
# Date 1513097220 -3600
# Node ID 725897bbabefce2e4fb31f66aecab0ec6250ec4a
# Parent  bc7a6455e12afb7ac9e9415962a047658a55b0aa
ensure separation of TeX tokens;

diff -r bc7a6455e12a -r 725897bbabef src/Pure/Thy/latex.ML
--- a/src/Pure/Thy/latex.ML	Tue Dec 12 16:12:48 2017 +0100
+++ b/src/Pure/Thy/latex.ML	Tue Dec 12 17:47:00 2017 +0100
@@ -189,7 +189,7 @@
       (case take_prefix is_blank_line (split_lines output) of
         (_, []) => output
       | (blank, rest) =>
-          cat_lines blank ^ "%\n" ^
+          cat_lines blank ^ " %\n" ^
           output_prop (Markup.lineN, Value.print_int n) ^
           cat_lines rest));