| Mon, 09 Sep 2024 21:32:11 +0200 | wenzelm | clarified Pretty.markup_block: use value-oriented YXML.output_markup, with final re-interpretation via print_mode in output_tree; | changeset | files |
| Mon, 09 Sep 2024 21:23:28 +0200 | wenzelm | minor performance tuning; | changeset | files |
| Mon, 09 Sep 2024 19:51:16 +0200 | wenzelm | unused; | changeset | files |
| Mon, 09 Sep 2024 19:40:18 +0200 | wenzelm | prefer static YXML.output_markup_only (without print_mode): Output.status is only relevant for PIDE (with print_mode "isabelle_process"); | changeset | files |