src/Pure/PIDE/rendering.scala
Tue, 29 Jul 2025 22:45:09 +0200 wenzelm minor performance tuning;
Tue, 29 Jul 2025 22:42:35 +0200 wenzelm clarified signature: builtin filter;
Tue, 29 Jul 2025 19:59:04 +0200 wenzelm clarified signature;
Mon, 28 Jul 2025 20:13:46 +0200 wenzelm clarified modules;
Sun, 27 Jul 2025 13:49:05 +0200 wenzelm clarified signature;
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;
less more (0) -100 -30 -10 -8 tip