src/Pure/General/file.ML
Tue, 03 Jan 2023 16:05:07 +0100 wenzelm clarified modules;
Fri, 24 Jun 2022 23:38:41 +0200 wenzelm clarified signature: File.read_lines is based on scalable Bytes.T;
Fri, 24 Jun 2022 23:31:28 +0200 wenzelm clarified modules;
Fri, 24 Jun 2022 11:20:14 +0200 wenzelm unused;
Thu, 23 Jun 2022 21:50:32 +0200 wenzelm more scalable generated files and code export, using Bytes.T;
Wed, 22 Jun 2022 16:25:22 +0200 wenzelm removed unused operations;
Wed, 22 Jun 2022 14:31:18 +0200 wenzelm tuned;
Tue, 21 Jun 2022 14:51:17 +0200 wenzelm tuned signature: more operations;
Tue, 21 Jun 2022 14:22:34 +0200 wenzelm tuned signature;
Mon, 20 Jun 2022 16:15:07 +0200 wenzelm clarified signature;
Sat, 27 Feb 2021 17:25:54 +0100 wenzelm more direct make_directory in ML and Scala, but ssh still requires perl for Windows UNC paths (see a5dbad753552);
Sat, 20 Feb 2021 23:01:35 +0100 wenzelm clarified modules;
Tue, 27 Oct 2020 22:34:37 +0100 wenzelm clarified signature: overloaded "+" for Path.append;
Sun, 20 Sep 2020 20:47:59 +0200 wenzelm clarified signature;
Sat, 02 Nov 2019 13:37:15 +0100 wenzelm back to more elementary Buffer.T -- less intermediate garbage;
less more (0) -100 -15 tip