src/Pure/PIDE/markup.scala
Tue, 29 Jul 2025 17:01:57 +0200 wenzelm more markup for batch build: command ranges with trailing whitespace;
Sun, 27 Jul 2025 16:41:25 +0200 wenzelm clarified signature;
Sun, 27 Jul 2025 16:28:10 +0200 wenzelm more direct support for "command_span" markup property "is_begin";
Sun, 29 Jun 2025 16:16:22 +0200 wenzelm clarified signature: more explicit operations;
Fri, 21 Mar 2025 18:37:05 +0100 wenzelm support for writeln_urgent, which is shown in Output before state messages (reminiscent of old Output.urgent_message before 521cea5fa777);
Mon, 23 Dec 2024 14:09:43 +0100 wenzelm tuned signature;
Wed, 18 Dec 2024 16:03:07 +0100 wenzelm more uniform Markup.notation vs. Markup.expression;
less more (0) -100 -30 -10 -7 tip