Wed, 13 Nov 2024 11:53:02 +0100 more ambitious scrolling: retain original scroll position if possible;
wenzelm [Wed, 13 Nov 2024 11:53:02 +0100] rev 81435
more ambitious scrolling: retain original scroll position if possible;
Wed, 13 Nov 2024 10:56:17 +0100 more ambitious scrolling: retain bottom position after output;
wenzelm [Wed, 13 Nov 2024 10:56:17 +0100] rev 81434
more ambitious scrolling: retain bottom position after output;
Tue, 12 Nov 2024 22:30:45 +0100 performance tuning: cache for Rich_Text.format, notably for incremental tracing;
wenzelm [Tue, 12 Nov 2024 22:30:45 +0100] rev 81433
performance tuning: cache for Rich_Text.format, notably for incremental tracing;
Tue, 12 Nov 2024 11:32:07 +0100 clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
wenzelm [Tue, 12 Nov 2024 11:32:07 +0100] rev 81432
clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -4 +4 +10 +30 +100 +300 tip