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;
less more (0) -100 -30 -10 -3 tip