| Tue, 27 Dec 2022 12:15:47 +0100 |
wenzelm |
clarified signature: avoid case class with mutable state;
|
file |
diff |
annotate
|
| Tue, 27 Dec 2022 12:00:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 26 Dec 2022 19:07:42 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 26 Dec 2022 18:41:27 +0100 |
wenzelm |
clarified signature: more position information via node_name;
|
file |
diff |
annotate
|
| Mon, 26 Dec 2022 16:44:13 +0100 |
wenzelm |
clarified signature: internalize errors (but: the parser rarely fails);
|
file |
diff |
annotate
|
| Mon, 26 Dec 2022 15:24:57 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 26 Dec 2022 15:11:42 +0100 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Mon, 26 Dec 2022 12:33:55 +0100 |
wenzelm |
clarified buffer_state: not synchronized, but exclusively owned by GUI thread;
|
file |
diff |
annotate
|
| Sat, 24 Dec 2022 13:19:39 +0100 |
wenzelm |
tuned signature: follow terminology of VSCode_Resources;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2022 22:41:47 +0100 |
wenzelm |
more robust Document.Pending_Edits: cover all nodes simulataneously, and thus support proper Snapshot.switch;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2022 15:42:52 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2022 15:34:09 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2022 15:29:29 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 20 Dec 2022 13:59:07 +0100 |
wenzelm |
clarified state of document model vs. document editor selection (again, see also a9d52d02bd83);
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 13:06:59 +0100 |
wenzelm |
clarified state change: presumably more robust;
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 12:22:47 +0100 |
wenzelm |
clarified state: node_required is guarded by PIDE.editor.document_active (e.g. open panel);
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 11:42:45 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2022 22:38:03 +0100 |
wenzelm |
clarified signature: proper scopes and types;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2022 21:41:26 +0100 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Mon, 07 Nov 2022 21:32:09 +0100 |
wenzelm |
clarified node_required status: distinguish theory_required vs. document_required;
|
file |
diff |
annotate
|
| Fri, 26 Aug 2022 11:57:05 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 21 Aug 2022 12:35:45 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 21 Aug 2022 12:19:38 +0200 |
wenzelm |
clarified names: Browser_Info.Config vs. Browser_Info.Context;
|
file |
diff |
annotate
|
| Sun, 21 Aug 2022 11:59:25 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 16:46:00 +0200 |
wenzelm |
clarified signature: support for adhoc file types;
|
file |
diff |
annotate
|
| Thu, 18 Aug 2022 11:43:27 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 17 Aug 2022 14:42:20 +0200 |
wenzelm |
clarified signature: avoid object-oriented HTML_Context;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 21:23:59 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 17:18:45 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Sat, 30 Jul 2022 13:44:26 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 23:19:12 +0200 |
wenzelm |
tuned formatting;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Thu, 31 Mar 2022 21:51:19 +0200 |
wenzelm |
tuned: avoid problems with scala3;
|
file |
diff |
annotate
|
| Fri, 25 Feb 2022 15:33:06 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 25 Feb 2022 14:42:38 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 25 Feb 2022 14:38:16 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 21 Feb 2022 14:33:41 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 21 Feb 2022 13:30:51 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 21 Feb 2022 12:56:35 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 20 Feb 2022 22:14:30 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 20 Feb 2022 15:30:07 +0100 |
wenzelm |
support for PDF.js: platform-independent PDF viewer;
|
file |
diff |
annotate
|
| Fri, 12 Nov 2021 16:49:28 +0100 |
wenzelm |
clarified HTML_Context: more explicit directory structure;
|
file |
diff |
annotate
|
| Fri, 12 Nov 2021 13:36:35 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 11 Nov 2021 22:06:18 +0100 |
wenzelm |
clarified signature: prefer static operations;
|
file |
diff |
annotate
|
| Fri, 05 Nov 2021 22:43:29 +0100 |
wenzelm |
avoid multiple copies of fonts;
|
file |
diff |
annotate
|
| Thu, 15 Jul 2021 22:07:56 +0200 |
wenzelm |
clarified global state: allow to deactivate main plugin;
|
file |
diff |
annotate
|
| Sun, 16 May 2021 13:34:27 +0200 |
wenzelm |
tuned signature --- following hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Wed, 31 Mar 2021 12:02:52 +0200 |
wenzelm |
more uniform HTTP resources;
|
file |
diff |
annotate
|
| Thu, 11 Mar 2021 20:30:56 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 21:04:27 +0100 |
wenzelm |
clarified signature --- fewer warnings;
|
file |
diff |
annotate
|
| Wed, 03 Mar 2021 22:48:46 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Tue, 05 Jan 2021 14:21:18 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sun, 03 Jan 2021 16:21:59 +0100 |
wenzelm |
clarified HTML presentation elements;
|
file |
diff |
annotate
|
| Sun, 20 Dec 2020 13:20:09 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 20 Dec 2020 12:32:12 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 20 Dec 2020 12:24:41 +0100 |
wenzelm |
tuned signature: more explicit types;
|
file |
diff |
annotate
|
| Sat, 19 Dec 2020 15:14:01 +0100 |
wenzelm |
clarified signature and module structure;
|
file |
diff |
annotate
|
| Sun, 29 Nov 2020 14:57:15 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 18 Nov 2020 15:52:12 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|