| Mon, 30 Jun 2025 12:42:21 +0200 |
wenzelm |
inline errors as "bad" markup;
|
file |
diff |
annotate
|
| Sun, 29 Jun 2025 15:53:45 +0200 |
wenzelm |
more robust: avoid crash on session database errors;
|
file |
diff |
annotate
|
| Sun, 29 Jun 2025 14:17:49 +0200 |
wenzelm |
basic support to reload theory markup from session store;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2025 17:12:41 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2025 16:24:58 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2025 15:45:55 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2025 12:27:43 +0200 |
wenzelm |
eliminate odd workaround from Aug-2012 (see 393a37003851);
|
file |
diff |
annotate
|
| Sat, 28 Jun 2025 12:22:03 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 28 Jun 2025 12:17:48 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 27 Jun 2025 15:31:55 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 08 Nov 2024 18:39:35 +0100 |
wenzelm |
clarified signature: avoid pointless alias (see also c82a1620b274 and 22aeec526ffd);
|
file |
diff |
annotate
|
| Wed, 04 Jan 2023 14:50:11 +0100 |
wenzelm |
tuned signature: avoid confusion with Document.Node.Blob and Command.Blob;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2023 14:35:19 +0100 |
wenzelm |
clarified signature: old node is ignored;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2023 13:21:45 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 11:42:45 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 21:19:05 +0100 |
wenzelm |
clarified signature --- fewer warnings;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 15:41:46 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 23:17:47 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Sun, 10 Jan 2021 13:04:29 +0100 |
wenzelm |
more informative errors: simplify diagnosis of spurious failures reported by users;
|
file |
diff |
annotate
|
| Fri, 27 Mar 2020 22:01:27 +0100 |
wenzelm |
misc tuning based on hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Mon, 07 Oct 2019 11:35:43 +0200 |
wenzelm |
discontinued pointless dump_checkpoint and share_common_data -- superseded by base logic image in Isabelle/MMT;
|
file |
diff |
annotate
|
| Mon, 02 Sep 2019 11:46:27 +0200 |
wenzelm |
clarified signature: prefer operations without position;
|
file |
diff |
annotate
|
| Wed, 28 Aug 2019 22:59:49 +0200 |
wenzelm |
support for share_common_data after define_command and before actual update: this affects string particles of command tokens;
|
file |
diff |
annotate
|
| Mon, 31 Dec 2018 20:08:32 +0100 |
wenzelm |
tuned;
|
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
|
| Thu, 31 May 2018 22:27:13 +0200 |
wenzelm |
Document.update includes node consolidation / presentation as regular print operation: avoid user operations on protocol thread;
|
file |
diff |
annotate
|
| Fri, 06 Oct 2017 21:23:21 +0200 |
wenzelm |
even more robust syntax (amending 122df1fde073);
|
file |
diff |
annotate
|
| Fri, 06 Oct 2017 17:13:57 +0200 |
wenzelm |
clarified node_syntax (amending ae38b8c0fdd9): default to overall_syntax, e.g. relevant for command spans wrt. bad header;
|
file |
diff |
annotate
|