# HG changeset patch
# User wenzelm
# Date 1726139366 -7200
# Node ID 32d0a41eea25df929212f8324a71dad53fd444a9
# Parent  8c67b14fdd480dab15a45ef918c47e2bce73b0fc
tuned signature;

diff -r 8c67b14fdd48 -r 32d0a41eea25 src/Pure/General/pretty.ML
--- a/src/Pure/General/pretty.ML	Wed Sep 11 23:26:25 2024 +0200
+++ b/src/Pure/General/pretty.ML	Thu Sep 12 13:09:26 2024 +0200
@@ -220,7 +220,7 @@
 
 (*default via print_mode*)
 fun output_ops opt_margin =
-  if print_mode_active Print_Mode.PIDE then symbolic_output_ops
+  if Print_Mode.PIDE_enabled () then symbolic_output_ops
   else pure_output_ops opt_margin;
 
 fun output_newline (ops: output_ops) = #1 (#output ops "\n");
diff -r 8c67b14fdd48 -r 32d0a41eea25 src/Pure/General/print_mode.ML
--- a/src/Pure/General/print_mode.ML	Wed Sep 11 23:26:25 2024 +0200
+++ b/src/Pure/General/print_mode.ML	Thu Sep 12 13:09:26 2024 +0200
@@ -25,6 +25,7 @@
   val setmp: string list -> ('a -> 'b) -> 'a -> 'b
   val with_modes: string list -> ('a -> 'b) -> 'a -> 'b
   val add_modes: string list -> unit
+  val PIDE_enabled: unit -> bool
 end;
 
 structure Print_Mode: PRINT_MODE =
@@ -54,6 +55,8 @@
 
 fun add_modes modes = Unsynchronized.change print_mode (append modes);
 
+fun PIDE_enabled () = print_mode_active PIDE;
+
 end;
 
 structure Basic_Print_Mode: BASIC_PRINT_MODE = Print_Mode;
diff -r 8c67b14fdd48 -r 32d0a41eea25 src/Pure/PIDE/markup.ML
--- a/src/Pure/PIDE/markup.ML	Wed Sep 11 23:26:25 2024 +0200
+++ b/src/Pure/PIDE/markup.ML	Thu Sep 12 13:09:26 2024 +0200
@@ -851,7 +851,7 @@
 val no_output = ("", "");
 
 fun output m =
-  if not (is_empty m) andalso print_mode_active Print_Mode.PIDE
+  if not (is_empty m) andalso Print_Mode.PIDE_enabled ()
   then YXML.output_markup m else no_output;
 
 fun markup m = output m |-> Library.enclose;