src/Pure/PIDE/command.scala
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;
Sun, 10 Mar 2019 00:21:34 +0100 wenzelm added semantic document markers;
Fri, 11 Jan 2019 22:34:28 +0100 wenzelm more operations;
Sat, 18 Aug 2018 12:41:05 +0200 wenzelm clarified modules;
Tue, 31 Jul 2018 21:11:24 +0200 wenzelm clarified ignored span / core range: include formal comments, e.g. relevant for error messages from antiquotations;
Tue, 31 Jul 2018 21:06:09 +0200 wenzelm tuned signature;
Tue, 05 Jun 2018 16:12:26 +0200 wenzelm less wasteful consolidation, based on PIDE front-end state and recent changes;
Thu, 31 May 2018 22:10:06 +0200 wenzelm clarified: consolidated result is last command;
Tue, 29 May 2018 22:25:59 +0200 wenzelm more node status information;
Mon, 28 May 2018 17:40:34 +0200 wenzelm clarified signature: Known.theories retains Document.Node.Entry (with header);
Tue, 08 May 2018 11:47:41 +0200 wenzelm more robust: self-export only;
Mon, 07 May 2018 17:11:01 +0200 wenzelm store exports within PIDE command state;
Sun, 11 Mar 2018 20:56:42 +0100 wenzelm tuned;
Sun, 11 Mar 2018 20:47:17 +0100 wenzelm update XML cache for slightly modified messages;
Sun, 11 Mar 2018 20:31:25 +0100 wenzelm more compact markup tree: output messages are already stored in command results (e.g. relevant for XML data representation);
Tue, 16 Jan 2018 11:27:52 +0100 wenzelm discontinued old form of marginal comments;
Tue, 31 Oct 2017 19:29:24 +0100 wenzelm clarified signature;
Thu, 05 Oct 2017 17:37:47 +0200 wenzelm completion supports theory header imports;
Tue, 08 Aug 2017 22:13:05 +0200 wenzelm maintain "consolidated" status of theory nodes, which means all evals are finished (but not necessarily prints nor imports);
Thu, 20 Apr 2017 11:38:42 +0200 wenzelm tuned signature;
Mon, 17 Apr 2017 12:20:45 +0200 wenzelm tuned signature;
Mon, 03 Apr 2017 16:36:45 +0200 wenzelm provide session qualifier via resources;
Sat, 01 Apr 2017 15:35:32 +0200 wenzelm tuned signature;
Mon, 20 Mar 2017 20:43:26 +0100 wenzelm support to encode/decode command state;
Sat, 07 Jan 2017 20:37:48 +0100 wenzelm more uniform node_header (non-strict);
Sat, 07 Jan 2017 20:01:05 +0100 wenzelm tuned signature;
Sat, 07 Jan 2017 19:36:40 +0100 wenzelm tuned signature;
Thu, 05 Jan 2017 16:16:18 +0100 wenzelm suppress empty results;
Mon, 07 Nov 2016 19:09:10 +0100 wenzelm more uniform path syntax, as in ML (see 5a7c919a4ada);
Tue, 02 Aug 2016 18:45:34 +0200 wenzelm tuned signature -- prover-independence is presently theoretical;
Wed, 13 Apr 2016 18:01:05 +0200 wenzelm eliminated "xname" and variants;
Wed, 13 Apr 2016 11:31:13 +0200 wenzelm clarified syntax;
Thu, 05 Nov 2015 00:02:30 +0100 wenzelm symbolic syntax "\<comment> text";
Sat, 19 Sep 2015 21:07:37 +0200 wenzelm straight-forward refresh, without special preconditions;
Wed, 12 Aug 2015 13:53:51 +0200 wenzelm resolve undefined blobs by default, e.g. relevant for ML debugger to avoid reset of breakpoints after reload;
Sun, 03 May 2015 00:01:10 +0200 wenzelm misc tuning, based on warnings by IntelliJ IDEA;
Sat, 04 Apr 2015 21:21:40 +0200 wenzelm more general notion of command span: command keyword not necessarily at start;
Tue, 17 Mar 2015 15:21:41 +0100 wenzelm misc tuning and simplification;
Mon, 16 Mar 2015 13:32:31 +0100 wenzelm avoid duplicate header errors, more precise positions;
Mon, 16 Mar 2015 11:07:56 +0100 wenzelm clarified modules;
Sun, 15 Mar 2015 22:15:08 +0100 wenzelm more markup, which helps to create missing imports;
Sun, 15 Mar 2015 21:57:10 +0100 wenzelm proper command id for inlined errors, which is important for Command.State.accumulate;
less more (0) -100 -60 tip