--- 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");
--- 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;
--- 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;