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