src/Pure/PIDE/command.scala
Mon, 30 Jun 2025 12:42:21 +0200 wenzelm inline errors as "bad" markup;
Mon, 23 Jun 2025 13:55:09 +0200 wenzelm clarified signature;
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;
Tue, 12 Nov 2024 11:16:36 +0100 wenzelm omit redundant compact_source (see e1abca2527da): Command_Span.unparsed consists of one token with the original source;
Tue, 12 Nov 2024 11:04:54 +0100 wenzelm tuned;
Sun, 10 Nov 2024 15:11:04 +0100 wenzelm obsolete;
Sun, 10 Nov 2024 13:40:28 +0100 wenzelm minor performance tuning: avoid concatenation of existing string material;
less more (0) -100 -30 -10 -7 tip