# HG changeset patch
# User wenzelm
# Date 1513078501 -3600
# Node ID a58bbe66ac812857c503175d2309b026fb1af133
# Parent  d5e51ba2156159204621b876be84f29f36625fad
avoid excessive whitespace between antiquotations and text;

diff -r d5e51ba21561 -r a58bbe66ac81 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Mon Dec 11 18:39:24 2017 +0100
+++ b/src/Pure/Thy/thy_output.ML	Tue Dec 12 12:35:01 2017 +0100
@@ -211,8 +211,7 @@
     val output_antiquotes =
       map (fn ant =>
         eval_antiquote state ant
-        |> mark_range ? Latex.range_output (#1 (Antiquote.range [ant])))
-      #> cat_lines;
+        |> mark_range ? Latex.range_output (#1 (Antiquote.range [ant]))) #> implode;
 
     fun output_line line =
       (if Markdown.line_is_item line then "\\item " else "") ^
@@ -231,13 +230,13 @@
         val reports = Antiquote.antiq_reports ants;
         val blocks = Markdown.read_antiquotes ants;
         val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
-      in "%\n" ^ output_blocks blocks end
+      in output_blocks blocks end
     else
       let
         val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
         val reports = Antiquote.antiq_reports ants;
         val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
-      in "%\n" ^ output_antiquotes ants end
+      in output_antiquotes ants end
   end;
 
 
@@ -273,7 +272,8 @@
   | Markup_Env_Token (cmd, source) =>
       Latex.environment ("isamarkup" ^ cmd)
         (output_text state {markdown = true, mark_range = true} source)
-  | Raw_Token source => output_text state {markdown = true, mark_range = true} source ^ "\n");
+  | Raw_Token source =>
+      "%\n" ^ output_text state {markdown = true, mark_range = true} source ^ "\n");
 
 
 (* command spans *)