| Wed, 06 Aug 2025 10:55:41 +0200 |
wenzelm |
clarified output;
|
file |
diff |
annotate
|
| Tue, 25 Mar 2025 23:05:15 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Wed, 12 Feb 2025 00:40:57 +0100 |
wenzelm |
removed unused imports;
|
file |
diff |
annotate
|
| Sun, 02 Jul 2023 19:05:59 +0200 |
wenzelm |
tuned: prefer Scala over Java;
|
file |
diff |
annotate
|
| Sat, 01 Oct 2022 20:10:56 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 19 Jun 2017 17:28:48 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 20 Apr 2017 11:38:42 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 04 Apr 2017 18:43:58 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Sun, 12 Mar 2017 14:23:38 +0100 |
wenzelm |
discontinued pointless Text.Length: Javascript and Java agree in old-fashioned UTF-16;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2017 21:41:14 +0100 |
wenzelm |
suppress vacuous edits;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2017 20:30:05 +0100 |
wenzelm |
clarified native Text.Offset versus Text.Length index Int;
|
file |
diff |
annotate
|
| Wed, 08 Mar 2017 20:25:57 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Mon, 06 Mar 2017 17:10:37 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 07 Jan 2017 11:22:13 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2016 17:10:09 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 28 Dec 2016 11:28:31 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 10 Dec 2016 17:22:47 +0100 |
wenzelm |
clarified output: avoid confusion with line:column notation;
|
file |
diff |
annotate
|
| Mon, 24 Oct 2016 12:16:12 +0200 |
wenzelm |
discontinued unused / untested distinction of separate PIDE modules;
|
file |
diff |
annotate
|
| Sun, 03 May 2015 00:01:10 +0200 |
wenzelm |
misc tuning, based on warnings by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Tue, 21 Oct 2014 17:49:51 +0200 |
wenzelm |
some structure matching, based on line token iterators;
|
file |
diff |
annotate
|
| Tue, 12 Aug 2014 15:46:20 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Wed, 23 Jul 2014 16:20:07 +0200 |
wenzelm |
more explicit treatment of cleared nodes (removal is implicit);
|
file |
diff |
annotate
|
| Sat, 26 Apr 2014 13:34:10 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Tue, 15 Apr 2014 16:44:06 +0200 |
wenzelm |
clarified treatment of markup ranges wrt. revert/convert: inflate_singularity allows to retrieve information like language_context more reliably during editing;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 20:03:00 +0200 |
wenzelm |
simplified Text.Chunk -- eliminated ooddities;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 19:17:28 +0200 |
wenzelm |
accumulate markup reports for "other" command ids, which are later retargeted and merged for rendering (in erratic order);
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 16:07:02 +0200 |
wenzelm |
avoid data redundancy;
|
file |
diff |
annotate
|
| Tue, 08 Apr 2014 15:12:54 +0200 |
wenzelm |
tuned signature -- moved Command.Chunk to Text.Chunk;
|
file |
diff |
annotate
|