| Fri, 20 Jan 2023 13:53:45 +0100 |
wenzelm |
obsolete (see also 01c9b3033036);
|
file |
diff |
annotate
|
| Sun, 15 Jan 2023 20:38:27 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sun, 15 Jan 2023 20:20:59 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 06 Jan 2023 17:20:53 +0100 |
wenzelm |
proper treatment of unicode_symbols;
|
file |
diff |
annotate
|
| Fri, 06 Jan 2023 16:54:16 +0100 |
wenzelm |
tuned signature: avoid alias that is unclear wrt. lazy state and Symbol.encode/decode status;
|
file |
diff |
annotate
|
| Fri, 06 Jan 2023 16:43:51 +0100 |
wenzelm |
tuned signature: more uniform operations;
|
file |
diff |
annotate
|
| Fri, 06 Jan 2023 14:58:13 +0100 |
wenzelm |
more uniform operations;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2023 17:00:22 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2023 16:44:15 +0100 |
wenzelm |
clarified session sources: theory and blobs are read from database, instead of physical file-system;
|
file |
diff |
annotate
|
| Thu, 05 Jan 2023 12:43:05 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2023 15:53:36 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 04 Jan 2023 15:42:00 +0100 |
wenzelm |
more direct access to session_sources, without somewhat fragile file-system operations;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2023 16:05:07 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2023 15:03:48 +0100 |
wenzelm |
clarified master_dir: avoid somewhat fragile Document.Node.Name.master_dir_path;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2023 12:58:00 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 02 Jan 2023 20:39:21 +0100 |
wenzelm |
clarified signature: more explicit types;
|
file |
diff |
annotate
|
| Mon, 02 Jan 2023 20:24:43 +0100 |
wenzelm |
more robust: prefer internal theory names;
|
file |
diff |
annotate
|
| Mon, 02 Jan 2023 16:02:16 +0100 |
wenzelm |
clarified session_sources (again, see also 9d0e6ea7aa68);
|
file |
diff |
annotate
|
| Mon, 02 Jan 2023 12:29:08 +0100 |
wenzelm |
clarified signature: uniform master_dir instead of separate field;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2022 15:42:13 +0100 |
wenzelm |
tunes signature;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2022 12:16:22 +0100 |
wenzelm |
tuned: no need to map master_dir, which does not participate in comparison;
|
file |
diff |
annotate
|
| Fri, 30 Dec 2022 20:26:28 +0100 |
wenzelm |
clarified generic path operations;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2022 22:11:16 +0100 |
wenzelm |
more accurate error messages;
|
file |
diff |
annotate
|
| Wed, 21 Dec 2022 13:52:44 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 17 Dec 2022 19:44:14 +0100 |
wenzelm |
clarified signature: avoid confusion due to redundant standard_path, which is already used here (but not elsewhere);
|
file |
diff |
annotate
|
| Sat, 17 Dec 2022 19:06:40 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 17 Dec 2022 17:28:05 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2022 18:12:48 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2022 17:51:52 +0100 |
wenzelm |
clarified names;
|
file |
diff |
annotate
|
| Fri, 16 Dec 2022 17:30:29 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|