# HG changeset patch
# User wenzelm
# Date 1726086522 -7200
# Node ID af34fcf7215df768fed1bcde11a4cb6c8aaa4b42
# Parent  ab0234b9af65925f866fd1cc712dd12b6302abac
tuned signature: more operations;

diff -r ab0234b9af65 -r af34fcf7215d NEWS
--- 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
diff -r ab0234b9af65 -r af34fcf7215d src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Sep 11 21:41:33 2024 +0200
+++ b/src/Pure/General/pretty.ML	Wed Sep 11 22:28:42 2024 +0200
@@ -77,6 +77,7 @@
   val output: output_ops -> T -> Bytes.T
   val string_of_ops: output_ops -> T -> string
   val string_of: T -> string
+  val pure_string_of: T -> string
   val writeln: T -> unit
   val markup_chunks: Markup.T -> T list -> T
   val chunks: T list -> T
@@ -428,6 +429,8 @@
 fun string_of_ops ops = Bytes.content o output ops;
 fun string_of prt = string_of_ops (output_ops NONE) prt;
 
+val pure_string_of = string_of_ops (pure_output_ops NONE);
+
 fun writeln prt =
   Output.writelns (Bytes.contents (output (output_ops NONE) prt));