src/Pure/General/file.scala
Fri, 24 Nov 2023 11:10:31 +0100 wenzelm more robust exception handling (amending 8cc1ae43e12e);
Thu, 23 Nov 2023 11:40:49 +0100 wenzelm clarified signature: avoid deprecated URL constructors;
Sun, 12 Nov 2023 12:26:08 +0100 wenzelm tuned signature: more operations;
Sat, 11 Nov 2023 22:05:37 +0100 wenzelm clarified modules;
Tue, 11 Jul 2023 11:37:23 +0200 wenzelm clarified signature, with subtle change of semantics (amending 8b5a2e4b16d4);
Sun, 02 Jul 2023 19:05:59 +0200 wenzelm tuned: prefer Scala over Java;
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;
less more (0) -100 -50 -30 tip