# HG changeset patch
# User wenzelm
# Date 1725972784 -7200
# Node ID 4d39ba5f82d63dadb012feefd3a310c884a82567
# Parent  1beb2dc3bf144b98065b13ad4a88fee40ebf45a4
clarified unbreakable latex output: Pretty.unformatted and (Pretty.string_of o Pretty.unbreakable) should coincide, but are produced by quite different means;

diff -r 1beb2dc3bf14 -r 4d39ba5f82d6 src/Pure/Thy/document_antiquotation.ML
--- a/src/Pure/Thy/document_antiquotation.ML	Tue Sep 10 12:34:32 2024 +0200
+++ b/src/Pure/Thy/document_antiquotation.ML	Tue Sep 10 14:53:04 2024 +0200
@@ -83,9 +83,10 @@
   Config.get ctxt thy_output_display ? Pretty.indent (Config.get ctxt thy_output_indent);
 
 fun format ctxt =
-  if Config.get ctxt thy_output_display orelse Config.get ctxt thy_output_break
-  then Pretty.string_of_ops (Pretty.output_ops (SOME (Config.get ctxt thy_output_margin)))
-  else Pretty.unformatted_string_of;
+  let
+    val breakable = Config.get ctxt thy_output_display orelse Config.get ctxt thy_output_break;
+    val ops = Pretty.output_ops (SOME (Config.get ctxt thy_output_margin));
+  in not breakable ? Pretty.unbreakable #> Pretty.string_of_ops ops end;
 
 fun output ctxt = delimit ctxt #> indent ctxt #> format ctxt #> Output.output;