src/Pure/PIDE/rendering.scala
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);
Thu, 26 Dec 2024 13:44:10 +0100 wenzelm clarified signature;
Thu, 26 Dec 2024 12:08:05 +0100 wenzelm clarified output;
Tue, 24 Dec 2024 14:59:56 +0100 wenzelm clarified signature;
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;
Sun, 08 Dec 2024 19:05:05 +0100 wenzelm tuned: more robust wrt. changes the Markup space;
Sun, 08 Dec 2024 11:49:55 +0100 wenzelm clarified signature;
Sat, 07 Dec 2024 23:40:29 +0100 wenzelm clarified signature;
Sat, 07 Dec 2024 23:50:18 +0100 wenzelm clarified term positions and markup: syntax = true means this is via concrete syntax;
Sat, 07 Dec 2024 21:42:59 +0100 wenzelm clarified signature: more explicit operations;
Thu, 07 Nov 2024 20:43:25 +0100 wenzelm more accurate message boundaries;
Thu, 07 Nov 2024 20:37:11 +0100 wenzelm tuned whitespace;
Thu, 07 Nov 2024 20:29:52 +0100 wenzelm clarified signature: more robust type XML.Elem;
less more (0) -100 -15 tip