Wed, 29 Nov 2023 15:27:21 +0100 |
wenzelm |
more compact representation;
|
file |
diff |
annotate
|
Wed, 11 Oct 2023 11:27:01 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Thu, 28 Sep 2023 14:43:07 +0200 |
wenzelm |
clarified treatment of exceptions: avoid catch-all handlers;
|
file |
diff |
annotate
|
Tue, 26 Sep 2023 13:34:04 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Tue, 08 Aug 2023 17:27:01 +0200 |
wenzelm |
tuned: more symmetric and more robust wrt. evolution of theory loader vs. PIDE state;
|
file |
diff |
annotate
|
Tue, 08 Aug 2023 17:17:42 +0200 |
wenzelm |
proper imports_keywords (amending 40a365360680), e.g. relevant for implicit "print_state" for commands defined after Pure;
|
file |
diff |
annotate
|
Mon, 27 Mar 2023 21:48:47 +0200 |
wenzelm |
performance tuning: prefer functor Set() over Table();
|
file |
diff |
annotate
|
Mon, 19 Dec 2022 11:42:45 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Sun, 06 Nov 2022 18:54:32 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 06 Nov 2022 15:28:56 +0100 |
wenzelm |
afford unconditional presentation, notably export_theory and present_thy, notably for HTML + PDF presentation within PIDE;
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 17:35:21 +0100 |
wenzelm |
tuned (again);
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 17:17:05 +0100 |
wenzelm |
prefer strict operation (see also f29056da5903);
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 17:14:41 +0100 |
wenzelm |
more antiquotations;
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 17:11:48 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 16:59:56 +0100 |
wenzelm |
prefer strict operation;
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 16:51:07 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 15:34:23 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 15:15:25 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 15:09:44 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 15:05:23 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 14:53:25 +0100 |
wenzelm |
misc tuning;
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 13:33:04 +0100 |
wenzelm |
clarified options;
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 11:38:01 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 04 Nov 2022 11:11:40 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 03 Nov 2022 20:42:27 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 03 Nov 2022 20:10:35 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Thu, 03 Nov 2022 16:08:28 +0100 |
wenzelm |
proper pattern (amending 40a365360680);
|
file |
diff |
annotate
|
Thu, 03 Nov 2022 16:03:44 +0100 |
wenzelm |
more timing;
|
file |
diff |
annotate
|
Thu, 03 Nov 2022 15:19:01 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Thu, 03 Nov 2022 12:50:53 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Wed, 02 Nov 2022 11:34:24 +0100 |
wenzelm |
more accurate outer syntax keywords (see also 94b2690ad494): base session could be anything, e.g. ZF vs. HOL;
|
file |
diff |
annotate
|
Wed, 02 Nov 2022 11:01:22 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Sun, 28 Aug 2022 14:55:40 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sun, 28 Aug 2022 14:44:34 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Sat, 04 Sep 2021 21:25:08 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Sun, 22 Aug 2021 19:21:54 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
Wed, 12 May 2021 16:47:52 +0200 |
wenzelm |
clarified signature: provide access to previous state;
|
file |
diff |
annotate
|
Sat, 19 Dec 2020 00:04:32 +0100 |
wenzelm |
clarified markup: open URL as editor file;
|
file |
diff |
annotate
|
Fri, 18 Dec 2020 23:30:29 +0100 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
Fri, 18 Dec 2020 23:19:07 +0100 |
wenzelm |
improved markup for theory header imports;
|
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 13:51:56 +0200 |
wenzelm |
more accurate context position reports;
|
file |
diff |
annotate
|
Wed, 02 Oct 2019 14:45:37 +0200 |
wenzelm |
more robust: avoid update/interrupt of long-running print_consolidation;
|
file |
diff |
annotate
|
Mon, 30 Sep 2019 17:28:40 +0200 |
wenzelm |
obsolete (see 030a6baa5cb2 and d14ddb1df52c);
|
file |
diff |
annotate
|
Fri, 13 Sep 2019 11:00:59 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 06 Sep 2019 19:44:54 +0200 |
wenzelm |
prefer commands_accepted: fewer protocol messages;
|
file |
diff |
annotate
|
Fri, 06 Sep 2019 17:10:23 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
Fri, 06 Sep 2019 16:48:28 +0200 |
wenzelm |
tuned signature -- prefer bulk messages;
|
file |
diff |
annotate
|
Mon, 26 Aug 2019 20:01:28 +0200 |
wenzelm |
added system option "execution_eager": potentially reduce resource requires for "isabelle mmt_import" (smaller subgraphs are finished and disposed earlier);
|
file |
diff |
annotate
|
Sun, 19 May 2019 18:10:45 +0200 |
wenzelm |
more thorough assignment, e.g. when "purge" removes commands that were not assigned;
|
file |
diff |
annotate
|
Sun, 19 May 2019 14:14:56 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
Sat, 18 May 2019 13:23:36 +0200 |
wenzelm |
tuned signature (following Scala version);
|
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
|
Sat, 01 Sep 2018 17:16:36 +0200 |
wenzelm |
clarified message;
|
file |
diff |
annotate
|
Sat, 01 Sep 2018 13:38:44 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
Fri, 29 Jun 2018 14:02:14 +0200 |
wenzelm |
always consolidate: allow errors in presentation;
|
file |
diff |
annotate
|
Tue, 05 Jun 2018 16:12:26 +0200 |
wenzelm |
less wasteful consolidation, based on PIDE front-end state and recent changes;
|
file |
diff |
annotate
|
Tue, 05 Jun 2018 14:15:49 +0200 |
wenzelm |
tuned -- short-circuit result;
|
file |
diff |
annotate
|