# HG changeset patch
# User wenzelm
# Date 1595793209 -7200
# Node ID 9c0b835d4cc2996f913d2afe84a274151c629a19
# Parent  f3e1144a1cec2bc9f2f122582093469089da17c6
proper pretty printing for latex output, notably for pide_session=true (default);

diff -r f3e1144a1cec -r 9c0b835d4cc2 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Sat Jul 25 23:23:59 2020 +0200
+++ b/src/Pure/General/pretty.ML	Sun Jul 26 21:53:29 2020 +0200
@@ -60,6 +60,7 @@
   val indent: int -> T -> T
   val unbreakable: T -> T
   val margin_default: int Unsynchronized.ref
+  val regularN: string
   val symbolicN: string
   val output_buffer: int option -> T -> Buffer.T
   val output: int option -> T -> Output.output
@@ -346,10 +347,12 @@
 
 val margin_default = Unsynchronized.ref ML_Pretty.default_margin;  (*right margin, or page width*)
 
+val regularN = "pretty_regular";
 val symbolicN = "pretty_symbolic";
 
 fun output_buffer margin prt =
-  if print_mode_active symbolicN then symbolic prt
+  if print_mode_active symbolicN andalso not (print_mode_active regularN)
+  then symbolic prt
   else formatted (the_default (! margin_default) margin) prt;
 
 val output = Buffer.content oo output_buffer;
diff -r f3e1144a1cec -r 9c0b835d4cc2 src/Pure/Thy/document_antiquotation.ML
--- a/src/Pure/Thy/document_antiquotation.ML	Sat Jul 25 23:23:59 2020 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML	Sun Jul 26 21:53:29 2020 +0200
@@ -181,7 +181,8 @@
     val _ = command pos (opts, src) preview_ctxt;
 
     val print_ctxt = Context_Position.set_visible false preview_ctxt;
-    val print_modes = space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN];
+    val print_modes =
+      space_explode "," (Config.get print_ctxt thy_output_modes) @ [Latex.latexN, Pretty.regularN];
   in [Print_Mode.with_modes print_modes (fn () => command pos (opts, src) print_ctxt) ()] end;
 
 in