| Tue, 31 Jan 2023 14:59:19 +0100 |
wenzelm |
defer build until document nodes are ready;
|
file |
diff |
annotate
|
| Tue, 31 Jan 2023 14:37:40 +0100 |
wenzelm |
clarified signature: prefer semantic status;
|
file |
diff |
annotate
|
| Tue, 31 Jan 2023 14:32:07 +0100 |
wenzelm |
removed obsolete parameter (see 7c23db6b857b);
|
file |
diff |
annotate
|
| Tue, 31 Jan 2023 12:27:00 +0100 |
wenzelm |
clarified Document_Editor.Session: more explicit types, more robust operations;
|
file |
diff |
annotate
|
| Mon, 30 Jan 2023 16:20:17 +0100 |
wenzelm |
clarified operation (without change of signature!);
|
file |
diff |
annotate
|
| Fri, 20 Jan 2023 13:08:54 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 18 Jan 2023 16:22:55 +0100 |
wenzelm |
tuned GUI;
|
file |
diff |
annotate
|
| Mon, 16 Jan 2023 20:57:38 +0100 |
wenzelm |
tuned GUI;
|
file |
diff |
annotate
|
| Mon, 16 Jan 2023 20:08:15 +0100 |
wenzelm |
more detailed Program_Progress / Log_Progress: each program gets its own log output, which is attached to the document via markup;
|
file |
diff |
annotate
|
| Sat, 24 Dec 2022 13:54:24 +0100 |
wenzelm |
clarified messages;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2022 23:18:28 +0100 |
wenzelm |
proper PIDE session background for interactive document context;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2022 22:11:16 +0100 |
wenzelm |
more accurate error messages;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2022 15:34:33 +0100 |
wenzelm |
actually build document;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2022 13:22:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2022 13:14:34 +0100 |
wenzelm |
clarified GUI;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2022 11:30:24 +0100 |
wenzelm |
more thorough GUI updates, notably for multiple Document dockables;
|
file |
diff |
annotate
|
| Tue, 20 Dec 2022 19:43:40 +0100 |
wenzelm |
more GUI operations;
|
file |
diff |
annotate
|
| Tue, 20 Dec 2022 19:19:44 +0100 |
wenzelm |
proper handling of state updates;
|
file |
diff |
annotate
|
| Tue, 20 Dec 2022 18:43:17 +0100 |
wenzelm |
clarified process management;
|
file |
diff |
annotate
|
| Tue, 20 Dec 2022 16:34:13 +0100 |
wenzelm |
clarified state document nodes for Theories_Status / Document_Dockable;
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 14:10:12 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 13:20:09 +0100 |
wenzelm |
more informative errors, including optional Exn.trace;
|
file |
diff |
annotate
|
| Mon, 19 Dec 2022 11:16:46 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 18 Dec 2022 18:30:37 +0100 |
wenzelm |
clarified state and process;
|
file |
diff |
annotate
|
| Sun, 18 Dec 2022 16:01:37 +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 22:11:36 +0100 |
wenzelm |
maintain global state of document editor views, notably for is_active operation;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2022 17:23:31 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 08 Dec 2022 14:02:59 +0100 |
wenzelm |
more specific GUI for document nodes;
|
file |
diff |
annotate
|
| Tue, 06 Dec 2022 16:38:50 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 06 Dec 2022 16:23:49 +0100 |
wenzelm |
more uniform session selectors, with persistent options;
|
file |
diff |
annotate
|
| Tue, 06 Dec 2022 14:41:13 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 05 Dec 2022 22:42:56 +0100 |
wenzelm |
tuned GUI behaviour;
|
file |
diff |
annotate
|
| Mon, 05 Dec 2022 22:31:46 +0100 |
wenzelm |
more GUI elements;
|
file |
diff |
annotate
|
| Mon, 05 Dec 2022 16:27:27 +0100 |
wenzelm |
clarified process: implicit load() when finished;
|
file |
diff |
annotate
|
| Mon, 05 Dec 2022 16:24:29 +0100 |
wenzelm |
more robust, notably initial update();
|
file |
diff |
annotate
|
| Mon, 05 Dec 2022 15:36:03 +0100 |
wenzelm |
tuned messages: implement "verbose = false", but there is no theory output anyway;
|
file |
diff |
annotate
|
| Thu, 10 Nov 2022 12:21:44 +0100 |
wenzelm |
clarified signature: ensure that entries are well-formed --- no consecutive separators, no separators at start/end;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2022 21:14:20 +0100 |
wenzelm |
more robust selection: avoid duplicates via "batch" number;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2022 19:42:21 +0100 |
wenzelm |
clarified GUI.Selector, with support for separator as pseudo-entry;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2022 14:20:52 +0100 |
wenzelm |
clarified GUI state;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2022 13:33:32 +0100 |
wenzelm |
clarified file names;
|
file |
diff |
annotate
|
| Wed, 09 Nov 2022 13:21:18 +0100 |
wenzelm |
clarified Log_Progress vs. GUI: more like Syslog_Dockable;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2022 10:58:46 +0200 |
wenzelm |
tuned GUI;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2022 10:54:12 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 01 Sep 2022 10:52:30 +0200 |
wenzelm |
clarified GUI behaviour;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2022 20:54:23 +0200 |
wenzelm |
clarified GUI update;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2022 20:46:55 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2022 20:41:30 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 31 Aug 2022 16:39:18 +0200 |
wenzelm |
more GUI functionality;
|
file |
diff |
annotate
|
| Tue, 30 Aug 2022 13:18:33 +0200 |
wenzelm |
clarified component structure, concerning initialization order;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 23:04:53 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 13 Aug 2022 12:32:38 +0200 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2022 20:20:53 +0200 |
wenzelm |
more GUI elements;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2022 12:50:19 +0200 |
wenzelm |
basic setup for document build panel;
|
file |
diff |
annotate
|