| changeset 80867 | 32d0a41eea25 |
| parent 80861 | 9de19e3a7231 |
| child 80905 | 47793a46d06c |
--- 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;