--- a/NEWS Wed Sep 11 21:41:33 2024 +0200
+++ b/NEWS Wed Sep 11 22:28:42 2024 +0200
@@ -91,6 +91,10 @@
variants), while the underlying Pretty.output operation supports an
explicit Pretty.output_ops argument for alternative applications.
+* Pretty.pure_output_ops and Pretty.pure_string_of support
+pretty-printed output without PIDE markup. This is occasionally useful
+for special tools, in contrast to regular user output.
+
* The print_mode "latex" only affects inner syntax variants, while its
impact on Output/Markup/Pretty operations has been removed. Thus the
print_mode operations Output.output and Output.escape have become