src/Pure/PIDE/command.ML
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;
Fri, 09 Oct 2015 21:16:00 +0200 wenzelm more direct HTML presentation, without print mode;
Mon, 21 Sep 2015 16:41:20 +0200 wenzelm option editor_output_state;
Mon, 21 Sep 2015 14:56:55 +0200 wenzelm separate panel for proof state output;
Mon, 29 Jun 2015 20:55:46 +0200 wenzelm improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
Thu, 16 Apr 2015 15:00:03 +0200 wenzelm more explicit bootstrap_thy;
Wed, 15 Apr 2015 14:54:25 +0200 wenzelm tuned messages;
Sun, 12 Apr 2015 11:23:36 +0200 wenzelm clarified language_path markup (again): exactly once *after* static phase, see also 83071f4c8ae6 and c043306d2598;
Tue, 07 Apr 2015 11:25:54 +0200 wenzelm recovered additional Markup.language_path from c043306d2598, which is important to override Markup.string from Command.read phase, and thus ensure that symbol completion is disabled;
Wed, 25 Mar 2015 11:39:52 +0100 wenzelm tuned signature;
Fri, 13 Mar 2015 12:58:49 +0100 wenzelm simplified Command.resolve_files in ML, using blobs_index from Scala;
Thu, 12 Mar 2015 22:00:51 +0100 wenzelm clarified markup for embedded files, early before execution;
less more (0) -100 -60 tip