src/Pure/General/file.scala
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";
Wed, 14 Nov 2018 20:04:39 +0100 wenzelm more uniform find_files, notably for symlinks;
Wed, 14 Nov 2018 16:26:58 +0100 wenzelm is_file/is_dir/read_dir: more uniform treatment of errors and boundary cases, notably for symlinks in ssh;
Wed, 14 Nov 2018 11:51:03 +0100 wenzelm clarified default (amending 72a9860f8602): avoid implicit change of File.find_files (it can have bad effects e.g. on "isabelle update_cartouches");
Tue, 13 Nov 2018 12:37:46 +0100 wenzelm clarified find_files: follow links by default, e.g. relevant for "~/cronjob/log";
Tue, 26 Sep 2017 16:12:21 +0200 wenzelm more operations;
Fri, 30 Jun 2017 14:17:48 +0200 wenzelm more operations;
Fri, 30 Jun 2017 14:01:55 +0200 wenzelm clarified signature;
Wed, 26 Apr 2017 16:13:05 +0200 wenzelm more robust treatment of non-UTF8 text files (cf. 3ed43cfc8b14), notably old log files in ISO-8859-15;
Sun, 22 Jan 2017 15:02:06 +0100 wenzelm hardlink within JVM;
Sun, 22 Jan 2017 13:11:38 +0100 wenzelm clarified operation: include dirs as well;
Wed, 04 Jan 2017 12:03:45 +0100 wenzelm clarified file URIs;
Tue, 03 Jan 2017 14:45:50 +0100 wenzelm more liberal drive letter, for the sake of file:// URLs;
Tue, 03 Jan 2017 14:17:03 +0100 wenzelm clarified master_dir: file-URL;
Sun, 01 Jan 2017 11:47:27 +0100 wenzelm clarified modules;
Thu, 29 Dec 2016 14:43:25 +0100 wenzelm tuned comments;
Fri, 23 Dec 2016 20:06:54 +0100 wenzelm proper file:// URL for external references;
Thu, 10 Nov 2016 21:54:58 +0100 wenzelm clarified File.move: target directory like File.copy;
Sat, 22 Oct 2016 16:39:27 +0200 wenzelm permissive rename operation (amending b265dd04d57d);
Tue, 18 Oct 2016 16:03:30 +0200 wenzelm clarified modules;
Sat, 15 Oct 2016 11:38:03 +0200 wenzelm prefer Isabelle standard Path;
Fri, 14 Oct 2016 21:34:52 +0200 wenzelm more operations;
Fri, 14 Oct 2016 20:53:10 +0200 wenzelm clarified file operations;
Mon, 03 Oct 2016 12:24:22 +0200 wenzelm tuned signature;
Mon, 03 Oct 2016 10:51:51 +0200 wenzelm clarified modules;
less more (0) -50 -30 tip