src/Pure/PIDE/document.ML
Wed, 29 Nov 2023 15:27:21 +0100 wenzelm more compact representation;
Wed, 11 Oct 2023 11:27:01 +0200 wenzelm clarified signature;
Thu, 28 Sep 2023 14:43:07 +0200 wenzelm clarified treatment of exceptions: avoid catch-all handlers;
Tue, 26 Sep 2023 13:34:04 +0200 wenzelm tuned;
Tue, 08 Aug 2023 17:27:01 +0200 wenzelm tuned: more symmetric and more robust wrt. evolution of theory loader vs. PIDE state;
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;
Mon, 27 Mar 2023 21:48:47 +0200 wenzelm performance tuning: prefer functor Set() over Table();
Mon, 19 Dec 2022 11:42:45 +0100 wenzelm clarified signature;
Sun, 06 Nov 2022 18:54:32 +0100 wenzelm tuned;
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;
Fri, 04 Nov 2022 17:35:21 +0100 wenzelm tuned (again);
Fri, 04 Nov 2022 17:17:05 +0100 wenzelm prefer strict operation (see also f29056da5903);
Fri, 04 Nov 2022 17:14:41 +0100 wenzelm more antiquotations;
Fri, 04 Nov 2022 17:11:48 +0100 wenzelm tuned;
Fri, 04 Nov 2022 16:59:56 +0100 wenzelm prefer strict operation;
Fri, 04 Nov 2022 16:51:07 +0100 wenzelm tuned;
Fri, 04 Nov 2022 15:34:23 +0100 wenzelm tuned signature;
Fri, 04 Nov 2022 15:15:25 +0100 wenzelm tuned signature;
Fri, 04 Nov 2022 15:09:44 +0100 wenzelm tuned;
Fri, 04 Nov 2022 15:05:23 +0100 wenzelm tuned;
Fri, 04 Nov 2022 14:53:25 +0100 wenzelm misc tuning;
Fri, 04 Nov 2022 13:33:04 +0100 wenzelm clarified options;
Fri, 04 Nov 2022 11:38:01 +0100 wenzelm tuned;
Fri, 04 Nov 2022 11:11:40 +0100 wenzelm tuned;
Thu, 03 Nov 2022 20:42:27 +0100 wenzelm tuned;
Thu, 03 Nov 2022 20:10:35 +0100 wenzelm clarified signature;
Thu, 03 Nov 2022 16:08:28 +0100 wenzelm proper pattern (amending 40a365360680);
Thu, 03 Nov 2022 16:03:44 +0100 wenzelm more timing;
Thu, 03 Nov 2022 15:19:01 +0100 wenzelm tuned;
Thu, 03 Nov 2022 12:50:53 +0100 wenzelm tuned;
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;
Wed, 02 Nov 2022 11:01:22 +0100 wenzelm tuned signature;
Sun, 28 Aug 2022 14:55:40 +0200 wenzelm tuned;
Sun, 28 Aug 2022 14:44:34 +0200 wenzelm tuned;
Sat, 04 Sep 2021 21:25:08 +0200 wenzelm clarified signature;
Sun, 22 Aug 2021 19:21:54 +0200 wenzelm tuned signature;
Wed, 12 May 2021 16:47:52 +0200 wenzelm clarified signature: provide access to previous state;
Sat, 19 Dec 2020 00:04:32 +0100 wenzelm clarified markup: open URL as editor file;
Fri, 18 Dec 2020 23:30:29 +0100 wenzelm more robust;
Fri, 18 Dec 2020 23:19:07 +0100 wenzelm improved markup for theory header imports;
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 13:51:56 +0200 wenzelm more accurate context position reports;
Wed, 02 Oct 2019 14:45:37 +0200 wenzelm more robust: avoid update/interrupt of long-running print_consolidation;
Mon, 30 Sep 2019 17:28:40 +0200 wenzelm obsolete (see 030a6baa5cb2 and d14ddb1df52c);
Fri, 13 Sep 2019 11:00:59 +0200 wenzelm tuned;
Fri, 06 Sep 2019 19:44:54 +0200 wenzelm prefer commands_accepted: fewer protocol messages;
Fri, 06 Sep 2019 17:10:23 +0200 wenzelm clarified signature;
Fri, 06 Sep 2019 16:48:28 +0200 wenzelm tuned signature -- prefer bulk messages;
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);
Sun, 19 May 2019 18:10:45 +0200 wenzelm more thorough assignment, e.g. when "purge" removes commands that were not assigned;
Sun, 19 May 2019 14:14:56 +0200 wenzelm tuned whitespace;
Sat, 18 May 2019 13:23:36 +0200 wenzelm tuned signature (following Scala version);
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;
Sat, 01 Sep 2018 17:16:36 +0200 wenzelm clarified message;
Sat, 01 Sep 2018 13:38:44 +0200 wenzelm tuned;
Fri, 29 Jun 2018 14:02:14 +0200 wenzelm always consolidate: allow errors in presentation;
Tue, 05 Jun 2018 16:12:26 +0200 wenzelm less wasteful consolidation, based on PIDE front-end state and recent changes;
Tue, 05 Jun 2018 14:15:49 +0200 wenzelm tuned -- short-circuit result;
less more (0) -300 -100 -60 tip