avoid excessive whitespace between antiquotations and text;
authorwenzelm
Tue Dec 12 12:35:01 2017 +0100 (17 months ago)
changeset 67186a58bbe66ac81
parent 67185 d5e51ba21561
child 67187 3457d7d43ee9
avoid excessive whitespace between antiquotations and text;
src/Pure/Thy/thy_output.ML
     1.1 --- a/src/Pure/Thy/thy_output.ML	Mon Dec 11 18:39:24 2017 +0100
     1.2 +++ b/src/Pure/Thy/thy_output.ML	Tue Dec 12 12:35:01 2017 +0100
     1.3 @@ -211,8 +211,7 @@
     1.4      val output_antiquotes =
     1.5        map (fn ant =>
     1.6          eval_antiquote state ant
     1.7 -        |> mark_range ? Latex.range_output (#1 (Antiquote.range [ant])))
     1.8 -      #> cat_lines;
     1.9 +        |> mark_range ? Latex.range_output (#1 (Antiquote.range [ant]))) #> implode;
    1.10  
    1.11      fun output_line line =
    1.12        (if Markdown.line_is_item line then "\\item " else "") ^
    1.13 @@ -231,13 +230,13 @@
    1.14          val reports = Antiquote.antiq_reports ants;
    1.15          val blocks = Markdown.read_antiquotes ants;
    1.16          val _ = if is_reported then Position.reports (reports @ Markdown.reports blocks) else ();
    1.17 -      in "%\n" ^ output_blocks blocks end
    1.18 +      in output_blocks blocks end
    1.19      else
    1.20        let
    1.21          val ants = Antiquote.parse pos (Symbol_Pos.trim_blanks syms);
    1.22          val reports = Antiquote.antiq_reports ants;
    1.23          val _ = if is_reported then Position.reports (reports @ Markdown.text_reports ants) else ();
    1.24 -      in "%\n" ^ output_antiquotes ants end
    1.25 +      in output_antiquotes ants end
    1.26    end;
    1.27  
    1.28  
    1.29 @@ -273,7 +272,8 @@
    1.30    | Markup_Env_Token (cmd, source) =>
    1.31        Latex.environment ("isamarkup" ^ cmd)
    1.32          (output_text state {markdown = true, mark_range = true} source)
    1.33 -  | Raw_Token source => output_text state {markdown = true, mark_range = true} source ^ "\n");
    1.34 +  | Raw_Token source =>
    1.35 +      "%\n" ^ output_text state {markdown = true, mark_range = true} source ^ "\n");
    1.36  
    1.37  
    1.38  (* command spans *)