| Sat, 31 Dec 2022 12:38:48 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2022 12:35:00 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2022 12:25:34 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Sat, 31 Dec 2022 11:48:32 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 30 Dec 2022 20:38:29 +0100 |
wenzelm |
more robust: avoid detour via somewhat fragile Node.Name.path;
|
file |
diff |
annotate
|
| Tue, 27 Dec 2022 17:35:01 +0100 |
wenzelm |
support for generic File_Format.parse_data, with persistent result in document model;
|
file |
diff |
annotate
|
| Mon, 26 Dec 2022 15:11:42 +0100 |
wenzelm |
clarified signature: more explicit types;
|
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:20:53 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Fri, 23 Dec 2022 15:07:48 +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 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
|
| 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:35:49 +0100 |
wenzelm |
clarified signature: avoid case class with redefined equality;
|
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
|
| Sat, 01 Oct 2022 20:10:56 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 22 Sep 2022 17:24:50 +0200 |
wenzelm |
clarified signature: persistent Node.source / Snapshot.source;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 21:25:13 +0200 |
wenzelm |
more robust treatment of Document.Node.Name, following stored data;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 20:19:05 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2022 14:39:37 +0200 |
wenzelm |
unused (despite cf52379c0776);
|
file |
diff |
annotate
|
| Fri, 12 Aug 2022 14:33:50 +0200 |
wenzelm |
tuned, following hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2022 14:26:17 +0200 |
wenzelm |
unused (see 696819fe2424);
|
file |
diff |
annotate
|
| Fri, 05 Aug 2022 20:54:39 +0200 |
wenzelm |
clarified Document.Snapshot.all_exports: refer to material from this (virtual) session;
|
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, 04 Mar 2021 15:52:08 +0100 |
wenzelm |
tuned;
|
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
|