src/Pure/General/file.scala
Fri, 16 Jun 2023 14:01:30 +0200 wenzelm minor performance tuning: avoid external process;
Thu, 15 Jun 2023 15:04:23 +0200 wenzelm clarified signature;
Thu, 15 Jun 2023 14:28:17 +0200 wenzelm tuned signature;
Fri, 14 Apr 2023 22:55:01 +0200 wenzelm more direct hg_sync init via ssh (see also 721b3278c8e4);
Mon, 06 Feb 2023 16:29:19 +0100 wenzelm tuned signature;
Mon, 06 Feb 2023 10:03:55 +0100 wenzelm clarified signature;
Fri, 27 Jan 2023 15:43:45 +0100 wenzelm prefer strict operation: java.io.File.length returns 0 for non-existent file;
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;
Tue, 03 Jan 2023 16:05:07 +0100 wenzelm clarified modules;
Wed, 30 Nov 2022 21:36:06 +0100 wenzelm proper unzip with strip option, within the JVM;
Wed, 30 Nov 2022 15:03:31 +0100 wenzelm clarified signature: prefer Scala functions instead of shell scripts;
Fri, 25 Nov 2022 20:17:54 +0100 wenzelm proper treatment of tar.gz double-extension;
Fri, 25 Nov 2022 13:38:15 +0100 wenzelm clarified signature;
Fri, 21 Oct 2022 18:06:32 +0200 wenzelm clarified signature;
Fri, 21 Oct 2022 16:39:31 +0200 wenzelm generic support for XZ and Zstd compression in Isabelle/Scala;
Fri, 21 Oct 2022 13:15:24 +0200 wenzelm clarified Zstd.init(): avoid accidential com.github.luben.zstd.util.Native.load() operation;
Fri, 21 Oct 2022 11:08:01 +0200 wenzelm support for Zstd data compression;
Fri, 19 Aug 2022 16:46:00 +0200 wenzelm clarified signature: support for adhoc file types;
Fri, 12 Aug 2022 16:08:12 +0200 wenzelm clarified signature --- simplified types;
Fri, 12 Aug 2022 16:01:52 +0200 wenzelm tuned signature;
Fri, 12 Aug 2022 15:57:22 +0200 wenzelm proper toString for Content_XML, which is not covered by trait Content;
Wed, 27 Jul 2022 09:03:06 +0200 wenzelm clarified signature;
Tue, 12 Jul 2022 14:38:31 +0200 wenzelm clarified signature;
Mon, 11 Jul 2022 15:22:17 +0200 wenzelm clarified signature;
Wed, 01 Jun 2022 10:07:00 +0200 wenzelm more robust;
Fri, 01 Apr 2022 17:06:10 +0200 wenzelm clarified formatting, for the sake of scala3;
Fri, 04 Mar 2022 22:50:58 +0100 wenzelm tuned signature: more robust operation;
Thu, 03 Mar 2022 19:51:00 +0100 wenzelm proper init of non-existing file;
Thu, 03 Mar 2022 17:30:43 +0100 wenzelm clarified signature;
Thu, 03 Mar 2022 17:13:24 +0100 wenzelm tuned;
Thu, 03 Mar 2022 17:11:43 +0100 wenzelm clarified signature;
Wed, 17 Nov 2021 12:55:02 +0100 wenzelm clarified modules;
Thu, 08 Jul 2021 13:34:12 +0200 wenzelm tuned signature;
Thu, 01 Jul 2021 13:46:42 +0200 wenzelm clarified modules and signatures;
Wed, 30 Jun 2021 20:57:38 +0200 wenzelm support for Isabelle setup in pure Java;
Wed, 30 Jun 2021 15:35:39 +0200 wenzelm clarified package: towards stand-alone setup;
Wed, 30 Jun 2021 13:25:35 +0200 wenzelm clarified modules;
Mon, 10 May 2021 22:18:12 +0200 wenzelm put more resources into jedit_build component;
Wed, 05 May 2021 13:27:30 +0200 wenzelm clarified signature;
Mon, 12 Apr 2021 22:41:51 +0200 wenzelm clarified signature: avoid overlap of String vs. Bytes (both are CharSequence);
Thu, 04 Mar 2021 21:04:27 +0100 wenzelm clarified signature --- fewer warnings;
Mon, 01 Mar 2021 22:22:12 +0100 wenzelm tuned --- fewer warnings;
Sat, 27 Feb 2021 19:42:44 +0100 wenzelm tuned;
Sat, 27 Feb 2021 18:04:29 +0100 wenzelm clarified modules: more like ML;
Wed, 25 Nov 2020 12:34:08 +0100 wenzelm clarified: more uniform;
Wed, 11 Nov 2020 20:55:25 +0100 wenzelm more operations (as in Isabelle/ML);
Sun, 11 Oct 2020 14:01:32 +0200 wenzelm clarified signature;
Mon, 05 Oct 2020 22:49:46 +0200 wenzelm clarified signature;
Wed, 15 Jul 2020 12:30:25 +0200 wenzelm clarified signature;
Fri, 27 Mar 2020 22:01:27 +0100 wenzelm misc tuning based on hints by IntelliJ IDEA;
Mon, 09 Mar 2020 19:35:07 +0100 wenzelm more scalable output of YXML files;
Wed, 15 Jan 2020 13:22:16 +0100 wenzelm unused;
Thu, 14 Nov 2019 11:35:02 +0100 wenzelm clarified signature;
Mon, 04 Feb 2019 16:01:44 +0100 wenzelm more thorough File.set_executable, notably for Windows;
Mon, 04 Feb 2019 15:45:40 +0100 wenzelm added executable flag for exports;
Thu, 20 Dec 2018 22:56:36 +0100 wenzelm clarified signature;
Sat, 08 Dec 2018 21:13:47 +0100 wenzelm clarified operations: uniform sorting of results;
Wed, 05 Dec 2018 22:46:44 +0100 wenzelm more direct File.executable operation: avoid external process (on Unix);
Wed, 05 Dec 2018 21:15:18 +0100 wenzelm more direct File.link operation: avoid external process;
Mon, 03 Dec 2018 14:59:42 +0100 wenzelm static type for Library.using: avoid Java 11 warnings on "Illegal reflective access";
less more (0) -100 -60 tip