src/Pure/PIDE/command.scala
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;
Thu, 04 Mar 2021 15:59:28 +0100 wenzelm tuned --- fewer warnings;
Thu, 04 Mar 2021 15:41:46 +0100 wenzelm tuned --- fewer warnings;
Wed, 03 Mar 2021 22:31:11 +0100 wenzelm tuned --- fewer warnings;
Sun, 10 Jan 2021 13:04:29 +0100 wenzelm more informative errors: simplify diagnosis of spurious failures reported by users;
Sat, 09 Jan 2021 18:56:53 +0100 wenzelm discontinued odd absolute position (amending 85bcdd05c6d0, 1975f397eabb): it violates translation invariance of commands and may lead to redundant re-checking of PIDE document;
Sat, 02 Jan 2021 22:22:34 +0100 wenzelm clarified signature: absorb XZ.Cache into XML.Cache;
Sun, 20 Dec 2020 15:47:54 +0100 wenzelm present auxiliary files with PIDE markup;
Fri, 18 Dec 2020 23:19:07 +0100 wenzelm improved markup for theory header imports;
Thu, 10 Dec 2020 16:35:56 +0100 wenzelm clarified signature: more specific types;
Mon, 07 Dec 2020 21:49:39 +0100 wenzelm read theory with PIDE markup from session database;
Mon, 07 Dec 2020 19:45:52 +0100 wenzelm tuned signature;
Sun, 06 Dec 2020 13:03:26 +0100 wenzelm silently ignore markup that starts out as singularity, e.g. <language/> from empty ML file;
Sat, 05 Dec 2020 19:09:39 +0100 wenzelm proper span position for blobs in batch-build (but: practically irrelevant);
Sat, 05 Dec 2020 18:14:55 +0100 wenzelm proper treatment of singleton Position.Offset within blob (amending cb9d5af781b4);
Sat, 05 Dec 2020 14:36:41 +0100 wenzelm tuned;
Sat, 05 Dec 2020 12:43:21 +0100 wenzelm clarified signature, notably access to blob files;
Sat, 05 Dec 2020 12:14:40 +0100 wenzelm support for PIDE markup for auxiliary files ("blobs");
Wed, 02 Dec 2020 15:01:37 +0100 wenzelm clarified signature --- more explicit types;
Sun, 29 Nov 2020 16:45:29 +0100 wenzelm restrict report redirection to current node;
Sun, 29 Nov 2020 16:11:52 +0100 wenzelm tuned signature;
Sun, 29 Nov 2020 15:41:36 +0100 wenzelm clarified modules;
Sun, 29 Nov 2020 15:33:19 +0100 wenzelm tuned signature;
Sun, 29 Nov 2020 14:57:15 +0100 wenzelm clarified signature;
Sat, 28 Nov 2020 23:28:56 +0100 wenzelm clarified parsing vs. semantic errors;
Sat, 28 Nov 2020 15:53:46 +0100 wenzelm tuned signature --- more explicit types;
Fri, 27 Nov 2020 23:47:06 +0100 wenzelm more flexible syntax for theory load commands via Isabelle/Scala;
Fri, 27 Nov 2020 21:59:23 +0100 wenzelm clarified theory keywords: loaded_files are determined statically in Scala, but ML needs to do it semantically;
Fri, 27 Nov 2020 16:44:36 +0100 wenzelm more explicit types;
Fri, 27 Nov 2020 16:40:31 +0100 wenzelm unused (see 7634d33c1a79);
Fri, 27 Nov 2020 14:00:54 +0100 wenzelm clarified modules;
Thu, 26 Nov 2020 15:59:09 +0100 wenzelm clarified signature: initial markup is_empty, not init_markup;
Wed, 25 Nov 2020 16:14:16 +0100 wenzelm more complete report positions, notably for command 'back' (amending eca176f773e0);
Wed, 25 Nov 2020 15:24:55 +0100 wenzelm tuned signature;
Wed, 25 Nov 2020 13:22:34 +0100 wenzelm tuned;
Wed, 25 Nov 2020 13:12:31 +0100 wenzelm removed pointless case: messages should always carry proper position;
Mon, 23 Nov 2020 15:14:58 +0100 wenzelm support for PIDE markup in batch build (inactive due to pide_reports=false);
Wed, 02 Oct 2019 14:45:37 +0200 wenzelm more robust: avoid update/interrupt of long-running print_consolidation;
Mon, 16 Sep 2019 19:35:08 +0200 wenzelm clarified theory imports completion, based on session directories and current master directory (no support for local session-subdirectories);
Mon, 02 Sep 2019 11:46:27 +0200 wenzelm clarified signature: prefer operations without position;
Sun, 10 Mar 2019 21:12:29 +0100 wenzelm document markers are formal comments, and may thus occur anywhere in the command-span;
less more (0) -100 -60 tip