| Fri, 24 Nov 2023 11:10:31 +0100 |
wenzelm |
more robust exception handling (amending 8cc1ae43e12e);
|
file |
diff |
annotate
|
| Thu, 23 Nov 2023 11:40:49 +0100 |
wenzelm |
clarified signature: avoid deprecated URL constructors;
|
file |
diff |
annotate
|
| Sun, 12 Nov 2023 12:26:08 +0100 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Sat, 11 Nov 2023 22:05:37 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 11 Jul 2023 11:37:23 +0200 |
wenzelm |
clarified signature, with subtle change of semantics (amending 8b5a2e4b16d4);
|
file |
diff |
annotate
|
| Sun, 02 Jul 2023 19:05:59 +0200 |
wenzelm |
tuned: prefer Scala over Java;
|
file |
diff |
annotate
|
| Fri, 16 Jun 2023 14:01:30 +0200 |
wenzelm |
minor performance tuning: avoid external process;
|
file |
diff |
annotate
|
| Thu, 15 Jun 2023 15:04:23 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 15 Jun 2023 14:28:17 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 14 Apr 2023 22:55:01 +0200 |
wenzelm |
more direct hg_sync init via ssh (see also 721b3278c8e4);
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 16:29:19 +0100 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 06 Feb 2023 10:03:55 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2023 15:43:45 +0100 |
wenzelm |
prefer strict operation: java.io.File.length returns 0 for non-existent file;
|
file |
diff |
annotate
|
| Fri, 27 Jan 2023 15:33:21 +0100 |
wenzelm |
prefer typed bytes count, but retain toString of original Long for robustness of Java/Scala string composition;
|
file |
diff |
annotate
|
| Tue, 03 Jan 2023 16:05:07 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2022 21:36:06 +0100 |
wenzelm |
proper unzip with strip option, within the JVM;
|
file |
diff |
annotate
|
| Wed, 30 Nov 2022 15:03:31 +0100 |
wenzelm |
clarified signature: prefer Scala functions instead of shell scripts;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2022 20:17:54 +0100 |
wenzelm |
proper treatment of tar.gz double-extension;
|
file |
diff |
annotate
|
| Fri, 25 Nov 2022 13:38:15 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2022 18:06:32 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2022 16:39:31 +0200 |
wenzelm |
generic support for XZ and Zstd compression in Isabelle/Scala;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2022 13:15:24 +0200 |
wenzelm |
clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
|
file |
diff |
annotate
|
| Fri, 21 Oct 2022 11:08:01 +0200 |
wenzelm |
support for Zstd data compression;
|
file |
diff |
annotate
|
| Fri, 19 Aug 2022 16:46:00 +0200 |
wenzelm |
clarified signature: support for adhoc file types;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2022 16:08:12 +0200 |
wenzelm |
clarified signature --- simplified types;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2022 16:01:52 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Fri, 12 Aug 2022 15:57:22 +0200 |
wenzelm |
proper toString for Content_XML, which is not covered by trait Content;
|
file |
diff |
annotate
|
| Wed, 27 Jul 2022 09:03:06 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Tue, 12 Jul 2022 14:38:31 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 11 Jul 2022 15:22:17 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 01 Jun 2022 10:07:00 +0200 |
wenzelm |
more robust;
|
file |
diff |
annotate
|
| Fri, 01 Apr 2022 17:06:10 +0200 |
wenzelm |
clarified formatting, for the sake of scala3;
|
file |
diff |
annotate
|
| Fri, 04 Mar 2022 22:50:58 +0100 |
wenzelm |
tuned signature: more robust operation;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2022 19:51:00 +0100 |
wenzelm |
proper init of non-existing file;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2022 17:30:43 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2022 17:13:24 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Thu, 03 Mar 2022 17:11:43 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 17 Nov 2021 12:55:02 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 08 Jul 2021 13:34:12 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Thu, 01 Jul 2021 13:46:42 +0200 |
wenzelm |
clarified modules and signatures;
|
file |
diff |
annotate
|
| Wed, 30 Jun 2021 20:57:38 +0200 |
wenzelm |
support for Isabelle setup in pure Java;
|
file |
diff |
annotate
|
| Wed, 30 Jun 2021 15:35:39 +0200 |
wenzelm |
clarified package: towards stand-alone setup;
|
file |
diff |
annotate
|
| Wed, 30 Jun 2021 13:25:35 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Mon, 10 May 2021 22:18:12 +0200 |
wenzelm |
put more resources into jedit_build component;
|
file |
diff |
annotate
|
| Wed, 05 May 2021 13:27:30 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 12 Apr 2021 22:41:51 +0200 |
wenzelm |
clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
|
file |
diff |
annotate
|
| Thu, 04 Mar 2021 21:04:27 +0100 |
wenzelm |
clarified signature --- fewer warnings;
|
file |
diff |
annotate
|
| Mon, 01 Mar 2021 22:22:12 +0100 |
wenzelm |
tuned --- fewer warnings;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2021 19:42:44 +0100 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Sat, 27 Feb 2021 18:04:29 +0100 |
wenzelm |
clarified modules: more like ML;
|
file |
diff |
annotate
|
| Wed, 25 Nov 2020 12:34:08 +0100 |
wenzelm |
clarified: more uniform;
|
file |
diff |
annotate
|
| Wed, 11 Nov 2020 20:55:25 +0100 |
wenzelm |
more operations (as in Isabelle/ML);
|
file |
diff |
annotate
|
| Sun, 11 Oct 2020 14:01:32 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 05 Oct 2020 22:49:46 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Wed, 15 Jul 2020 12:30:25 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Fri, 27 Mar 2020 22:01:27 +0100 |
wenzelm |
misc tuning based on hints by IntelliJ IDEA;
|
file |
diff |
annotate
|
| Mon, 09 Mar 2020 19:35:07 +0100 |
wenzelm |
more scalable output of YXML files;
|
file |
diff |
annotate
|
| Wed, 15 Jan 2020 13:22:16 +0100 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Thu, 14 Nov 2019 11:35:02 +0100 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Mon, 04 Feb 2019 16:01:44 +0100 |
wenzelm |
more thorough File.set_executable, notably for Windows;
|
file |
diff |
annotate
|