changeset 80869 | 87395be1a299 |
parent 80867 | 32d0a41eea25 |
--- a/src/Pure/General/print_mode.ML Thu Sep 12 13:10:36 2024 +0200 +++ b/src/Pure/General/print_mode.ML Thu Sep 12 13:13:59 2024 +0200 @@ -55,7 +55,8 @@ fun add_modes modes = Unsynchronized.change print_mode (append modes); -fun PIDE_enabled () = print_mode_active PIDE; +fun PIDE_enabled () = + find_first (fn mode => mode = PIDE orelse mode = "") (print_mode_value ()) = SOME PIDE; end;