--- 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));