# HG changeset patch
# User wenzelm
# Date 1516356133 -3600
# Node ID d1697ac0fcd1e895ad7399a82d524a1611b6e710
# Parent  bc8a76d5839a04874e12c2ca9e2cf43cdd2f4f03
tuned;

diff -r bc8a76d5839a -r d1697ac0fcd1 src/Pure/Thy/thy_output.ML
--- a/src/Pure/Thy/thy_output.ML	Thu Jan 18 21:42:03 2018 +0100
+++ b/src/Pure/Thy/thy_output.ML	Fri Jan 19 11:02:13 2018 +0100
@@ -461,9 +461,6 @@
   then Document_Antiquotation.indent_lines ctxt #> typewriter ctxt
   else split_lines #> map (typewriter ctxt) #> lines #> Latex.block;
 
-
-(* pretty output *)
-
 fun pretty ctxt =
   map (Document_Antiquotation.output ctxt #> Latex.string) #> lines #> isabelle ctxt;
 
@@ -472,6 +469,9 @@
     pretty ctxt [pretty_text ctxt (space_implode " " (map Token.unparse (Token.args_of_src src)))]
   else pretty ctxt prts;
 
+
+(* antiquotation variants *)
+
 fun antiquotation_pretty name scan f =
   Document_Antiquotation.setup name scan
     (fn {context = ctxt, argument = x, ...} => pretty ctxt (f ctxt x));