src/Pure/GUI/rich_text.scala
Tue, 12 Nov 2024 22:30:45 +0100 wenzelm performance tuning: cache for Rich_Text.format, notably for incremental tracing;
Tue, 12 Nov 2024 11:32:07 +0100 wenzelm clarified persistent values: Command.Results does not suitable for caching, because it contains all other messages;
Mon, 11 Nov 2024 12:47:51 +0100 wenzelm clarified signature and modules;
Sun, 10 Nov 2024 15:10:51 +0100 wenzelm clarified: more uniform results;
Sun, 10 Nov 2024 12:56:38 +0100 wenzelm clarified signature and data storage: incremental lazy values;
Sun, 10 Nov 2024 12:33:20 +0100 wenzelm tuned comments;
Sun, 10 Nov 2024 12:29:32 +0100 wenzelm clarified signature;
Sun, 10 Nov 2024 12:23:41 +0100 wenzelm clarified modules;
Sun, 10 Nov 2024 12:15:31 +0100 wenzelm clarified margin operations (again, reverting 4794576828df);
Sun, 10 Nov 2024 11:55:36 +0100 wenzelm clarified modules;
less more (0) tip