Tue, 19 Nov 2024 15:25:11 +0100 wenzelm re-use Output_Area;
Tue, 19 Nov 2024 10:52:02 +0100 wenzelm re-use Output_Area with search results;
Tue, 19 Nov 2024 10:40:19 +0100 wenzelm re-use Output_Area with search results;
Tue, 19 Nov 2024 10:14:22 +0100 wenzelm more thorough init;
Tue, 19 Nov 2024 10:11:37 +0100 wenzelm clarified signature: prefer defaults for Output_Dockable (and its variants);
Tue, 19 Nov 2024 10:11:17 +0100 wenzelm unused;
Mon, 18 Nov 2024 16:48:11 +0100 wenzelm tuned output: formatting is pointless for proportional font;
(0) -30000 -10000 -3000 -1000 -300 -100 -30 -10 -7 +7 +10 +30 +100 +300 tip