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;
Sat, 09 Nov 2024 21:34:38 +0100 wenzelm Document.Snapshot: support for multiple snippet_commands;
Fri, 08 Nov 2024 18:39:35 +0100 wenzelm clarified signature: avoid pointless alias (see also c82a1620b274 and 22aeec526ffd);
Fri, 08 Nov 2024 18:34:33 +0100 wenzelm clarified signature;
Wed, 08 Nov 2023 12:00:29 +0100 wenzelm tuned signature;
Tue, 19 Sep 2023 19:48:54 +0200 wenzelm clarified signature;
Tue, 29 Aug 2023 12:53:28 +0200 wenzelm misc tuning: support "scalac -source 3.3";
Fri, 21 Jul 2023 17:06:53 +0200 wenzelm clarified signature: more operations;
Thu, 05 Jan 2023 17:14:29 +0100 wenzelm tuned signature;
Thu, 05 Jan 2023 17:00:22 +0100 wenzelm tuned signature;
Thu, 05 Jan 2023 16:44:15 +0100 wenzelm clarified session sources: theory and blobs are read from database, instead of physical file-system;
Wed, 04 Jan 2023 15:53:36 +0100 wenzelm tuned;
Wed, 04 Jan 2023 15:42:00 +0100 wenzelm more direct access to session_sources, without somewhat fragile file-system operations;
Wed, 04 Jan 2023 14:50:11 +0100 wenzelm tuned signature: avoid confusion with Document.Node.Blob and Command.Blob;
Tue, 03 Jan 2023 12:58:00 +0100 wenzelm clarified modules;
Sun, 01 Jan 2023 22:54:40 +0100 wenzelm tuned signature, following Url.append_path;
Fri, 30 Dec 2022 20:26:28 +0100 wenzelm clarified generic path operations;
Sun, 18 Dec 2022 16:01:37 +0100 wenzelm clarified signature;
Sat, 17 Dec 2022 11:33:13 +0100 wenzelm clarified signature;
Sun, 06 Nov 2022 19:25:48 +0100 wenzelm minor performance tuning;
Sat, 01 Oct 2022 16:07:05 +0200 wenzelm tuned, following hints by IntelliJ IDEA;
Wed, 31 Aug 2022 15:05:28 +0200 wenzelm clarified signature;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Thu, 04 Mar 2021 16:08:30 +0100 wenzelm tuned --- fewer warnings;
less more (0) -100 -50 -30 tip