src/Pure/PIDE/command.ML
Mon, 12 Apr 2021 18:29:34 +0200 wenzelm clarified signature: avoid tmp file;
Mon, 01 Mar 2021 18:31:11 +0100 wenzelm clarified signature, according to Isabelle/Scala;
Fri, 08 Jan 2021 16:59:27 +0100 wenzelm discontinued body_range (again): does not quite work, because Position.thread_data is plain Toplevel.pos_of only;
Fri, 08 Jan 2021 16:36:20 +0100 wenzelm clarified: command keyword position is sufficient (amending 693a39f2cddc);
Fri, 08 Jan 2021 15:03:51 +0100 wenzelm recovered body_range from eca176f773e0 --- its Command.core_range is in conflict with batch-build markup;
Fri, 08 Jan 2021 14:42:18 +0100 wenzelm tuned;
Fri, 08 Jan 2021 14:40:04 +0100 wenzelm support more command positions, analogous to Command.core_range in Isabelle/Scala;
Fri, 08 Jan 2021 14:29:58 +0100 wenzelm tuned;
Fri, 08 Jan 2021 14:05:46 +0100 wenzelm more uniform core_range (amending def3ec9cdb7e);
Mon, 04 Jan 2021 14:23:43 +0100 wenzelm tuned signature;
Sat, 19 Dec 2020 00:08:14 +0100 wenzelm download auxiliary files via "curl";
Fri, 18 Dec 2020 12:57:25 +0100 wenzelm clarified markup (refining dd56ba1974e6);
Mon, 07 Dec 2020 16:09:06 +0100 wenzelm more accurate markup (refining 1c59b555ac4a);
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, 03 Apr 2020 17:35:10 +0200 wenzelm less redundant markup reports;
Fri, 06 Sep 2019 16:48:28 +0200 wenzelm tuned signature -- prefer bulk messages;
Sun, 10 Mar 2019 21:31:28 +0100 wenzelm tuned -- Toplevel.presentation_context is total;
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;
Sat, 09 Mar 2019 23:57:07 +0100 wenzelm clarified signature;
Sat, 09 Mar 2019 13:19:13 +0100 wenzelm clarified Toplevel.state: more explicit types;
Wed, 20 Feb 2019 21:54:52 +0100 wenzelm physical vs. logical events, the latter takes GC time into account;
Wed, 26 Dec 2018 20:57:23 +0100 wenzelm {* verbatim *} is explicit legacy feature;
Fri, 07 Sep 2018 19:49:26 +0200 wenzelm proper tast_context (amending 5f44ad150ed8);
Sun, 02 Sep 2018 22:54:51 +0200 wenzelm more robust: avoid race-condition of terminated vs. consolidated;
Sun, 02 Sep 2018 22:30:08 +0200 wenzelm clarified quasi_consolidated state: ensure that exports are present for ok nodes;
Sun, 02 Sep 2018 14:56:26 +0200 wenzelm more robust reset_state: begin/end structure takes precedence over goal/proof structure;
Sun, 02 Sep 2018 13:21:15 +0200 wenzelm tuned;
Sat, 01 Sep 2018 20:20:50 +0200 wenzelm more explicit status for "canceled" command within theory node;
Sat, 01 Sep 2018 16:08:54 +0200 wenzelm more robust: memoize interrupt (e.g. resource problem) -- avoid multiple attempts;
Sat, 01 Sep 2018 14:25:03 +0200 wenzelm more robust eval_result: enforce finished result stemming from previous run_process, fail if that was interrupted (e.g. due to resource problems);
Thu, 30 Aug 2018 19:52:30 +0200 wenzelm more accurate position for auxiliary files;
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;
Sun, 03 Jun 2018 22:02:20 +0200 wenzelm fork parallel prints early in execution: avoid degradation of priority due to main eval task;
Fri, 01 Jun 2018 10:56:01 +0200 wenzelm clarified priority;
Thu, 31 May 2018 22:04:15 +0200 wenzelm support for anonymous print function values;
Wed, 30 May 2018 21:11:13 +0200 wenzelm tuned;
Mon, 14 May 2018 22:22:47 +0200 wenzelm support for dynamic document output while editing;
Wed, 09 May 2018 20:45:57 +0200 wenzelm clarified future scheduling parameters, with support for parallel_limit;
Sat, 03 Feb 2018 15:34:22 +0100 wenzelm just one check of formal comments;
Sat, 03 Feb 2018 14:39:17 +0100 wenzelm avoid proliferation of language_document reports;
Sun, 28 Jan 2018 19:28:52 +0100 wenzelm clarified take/drop/chop prefix/suffix;
Tue, 16 Jan 2018 11:27:52 +0100 wenzelm discontinued old form of marginal comments;
Mon, 08 Jan 2018 23:45:43 +0100 wenzelm theory Pure is default presentation context;
Mon, 08 Jan 2018 15:51:29 +0100 wenzelm check formal comments recursively, within arbitrary cartouches (unknown sublanguages);
Wed, 13 Dec 2017 16:18:40 +0100 wenzelm positions as postlude: avoid intrusion of odd %-forms into main tex source;
Tue, 12 Dec 2017 16:12:48 +0100 wenzelm simplified positions -- line is also human-readable in generated .tex file;
Mon, 11 Dec 2017 17:52:05 +0100 wenzelm more robust range on preceding comment-line;
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, 22 Jun 2017 15:20:32 +0200 wenzelm more informative task_statistics;
Sat, 27 May 2017 13:20:35 +0200 wenzelm clarified build errors;
Wed, 28 Dec 2016 10:39:50 +0100 wenzelm more uniform treatment of "bad" like other messages (with serial number);
Wed, 13 Jul 2016 15:23:33 +0200 wenzelm obsolete;
Wed, 13 Jul 2016 15:19:16 +0200 wenzelm semantic indentation for unstructured proof scripts;
Sat, 09 Apr 2016 14:11:31 +0200 wenzelm tuned signature -- closer to Exn.Interrupt.expose in Scala;
Wed, 06 Apr 2016 23:45:19 +0200 wenzelm treat ROOT.ML as theory with header "theory ML_Root imports ML_Bootstrap begin";
Sat, 02 Apr 2016 23:29:05 +0200 wenzelm prefer infix operations;
Thu, 03 Mar 2016 15:23:02 +0100 wenzelm clarified modules;
Fri, 16 Oct 2015 10:11:20 +0200 wenzelm clarified Antiquote.antiq_reports;
less more (0) -100 -60 tip