| Tue, 17 Oct 2023 12:10:58 +0200 |
wenzelm |
tuned signature, following Isabelle/Scala;
|
file |
diff |
annotate
|
| Thu, 28 Sep 2023 14:43:07 +0200 |
wenzelm |
clarified treatment of exceptions: avoid catch-all handlers;
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 21:46:38 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 25 Sep 2023 18:45:41 +0200 |
wenzelm |
clarified signature: avoid association with potentially dangerous Exn.capture;
|
file |
diff |
annotate
|
| Thu, 21 Sep 2023 23:45:03 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 09 Jul 2023 17:39:46 +0200 |
wenzelm |
more markup for command_span: this allows to reconstruct Thy_Element structure without knowing the outer syntax;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2022 16:49:43 +0100 |
wenzelm |
more uniform report of Markup.language_path;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2022 16:02:12 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 04 Nov 2022 17:14:41 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
| Fri, 04 Nov 2022 15:15:25 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 04 Nov 2022 11:11:40 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2022 20:53:21 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2022 20:33:59 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 03 Nov 2022 20:10:35 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 02 Nov 2022 09:47:27 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sun, 28 Aug 2022 20:21:47 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2022 23:05:37 +0200 |
wenzelm |
prefer scalable byte strings;
|
file |
diff |
annotate
|
| Mon, 06 Dec 2021 15:34:54 +0100 |
wenzelm |
discontinued old-style {* verbatim *} tokens;
|
file |
diff |
annotate
|
| Wed, 03 Nov 2021 16:23:20 +0100 |
wenzelm |
more PIDE markup;
|
file |
diff |
annotate
|
| Sun, 22 Aug 2021 19:21:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 21 May 2021 12:29:29 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 12 Apr 2021 18:29:34 +0200 |
wenzelm |
clarified signature: avoid tmp file;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 18:31:11 +0100 |
wenzelm |
clarified signature, according to Isabelle/Scala;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2021 16:36:20 +0100 |
wenzelm |
clarified: command keyword position is sufficient (amending 693a39f2cddc);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2021 14:42:18 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2021 14:40:04 +0100 |
wenzelm |
support more command positions, analogous to Command.core_range in Isabelle/Scala;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2021 14:29:58 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 08 Jan 2021 14:05:46 +0100 |
wenzelm |
more uniform core_range (amending def3ec9cdb7e);
|
file |
diff |
annotate
|
| Mon, 04 Jan 2021 14:23:43 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sat, 19 Dec 2020 00:08:14 +0100 |
wenzelm |
download auxiliary files via "curl";
|
file |
diff |
annotate
|
| Fri, 18 Dec 2020 12:57:25 +0100 |
wenzelm |
clarified markup (refining dd56ba1974e6);
|
file |
diff |
annotate
|
| Mon, 07 Dec 2020 16:09:06 +0100 |
wenzelm |
more accurate markup (refining 1c59b555ac4a);
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Fri, 03 Apr 2020 17:35:10 +0200 |
wenzelm |
less redundant markup reports;
|
file |
diff |
annotate
|
| Fri, 06 Sep 2019 16:48:28 +0200 |
wenzelm |
tuned signature -- prefer bulk messages;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 21:31:28 +0100 |
wenzelm |
tuned -- Toplevel.presentation_context is total;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 21:12:29 +0100 |
wenzelm |
document markers are formal comments, and may thus occur anywhere in the command-span;
|
file |
diff |
annotate
|
| Sun, 10 Mar 2019 00:21:34 +0100 |
wenzelm |
added semantic document markers;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 23:57:07 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 09 Mar 2019 13:19:13 +0100 |
wenzelm |
clarified Toplevel.state: more explicit types;
|
file |
diff |
annotate
|
| Wed, 20 Feb 2019 21:54:52 +0100 |
wenzelm |
physical vs. logical events, the latter takes GC time into account;
|
file |
diff |
annotate
|
| Wed, 26 Dec 2018 20:57:23 +0100 |
wenzelm |
{* verbatim *} is explicit legacy feature;
|
file |
diff |
annotate
|
| Fri, 07 Sep 2018 19:49:26 +0200 |
wenzelm |
proper tast_context (amending 5f44ad150ed8);
|
file |
diff |
annotate
|
| Sun, 02 Sep 2018 22:54:51 +0200 |
wenzelm |
more robust: avoid race-condition of terminated vs. consolidated;
|
file |
diff |
annotate
|
| Sun, 02 Sep 2018 22:30:08 +0200 |
wenzelm |
clarified quasi_consolidated state: ensure that exports are present for ok nodes;
|
file |
diff |
annotate
|
| Sun, 02 Sep 2018 14:56:26 +0200 |
wenzelm |
more robust reset_state: begin/end structure takes precedence over goal/proof structure;
|
file |
diff |
annotate
|
| Sun, 02 Sep 2018 13:21:15 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2018 20:20:50 +0200 |
wenzelm |
more explicit status for "canceled" command within theory node;
|
file |
diff |
annotate
|
| Sat, 01 Sep 2018 16:08:54 +0200 |
wenzelm |
more robust: memoize interrupt (e.g. resource problem) -- avoid multiple attempts;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Thu, 30 Aug 2018 19:52:30 +0200 |
wenzelm |
more accurate position for auxiliary files;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Tue, 31 Jul 2018 21:06:09 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 03 Jun 2018 22:02:20 +0200 |
wenzelm |
fork parallel prints early in execution: avoid degradation of priority due to main eval task;
|
file |
diff |
annotate
|
| Fri, 01 Jun 2018 10:56:01 +0200 |
wenzelm |
clarified priority;
|
file |
diff |
annotate
|
| Thu, 31 May 2018 22:04:15 +0200 |
wenzelm |
support for anonymous print function values;
|
file |
diff |
annotate
|
| Wed, 30 May 2018 21:11:13 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 14 May 2018 22:22:47 +0200 |
wenzelm |
support for dynamic document output while editing;
|
file |
diff |
annotate
|