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;
Mon, 27 May 2019 14:25:00 +0200 wenzelm tuned whitespace;
Wed, 19 Dec 2018 21:38:57 +0100 wenzelm more robust open/close bracket, but with potential danger of blocking indefinitely in uninterruptible state;
Sat, 08 Dec 2018 21:13:47 +0100 wenzelm clarified operations: uniform sorting of results;
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;
Sat, 03 Nov 2018 19:31:15 +0100 wenzelm more operations;
Thu, 29 Dec 2016 14:43:25 +0100 wenzelm tuned comments;
Tue, 18 Oct 2016 16:03:30 +0200 wenzelm clarified modules;
Thu, 11 Aug 2016 18:26:16 +0200 wenzelm tuned error;
Mon, 04 Apr 2016 20:45:54 +0200 wenzelm allow empty string;
Mon, 07 Mar 2016 21:53:21 +0100 wenzelm discontinued cd, pwd;
Mon, 07 Mar 2016 21:09:28 +0100 wenzelm File.bash_string operations in ML as in Scala -- exclusively for GNU bash, not perl and not user output;
Mon, 29 Feb 2016 15:39:17 +0100 wenzelm clarified modules;
Thu, 20 Aug 2015 13:41:53 +0200 wenzelm precise BinIO, without newline conversion on Windows;
Tue, 18 Aug 2015 16:08:47 +0200 wenzelm clarified File.standard_path vs. File.platform_path (like Isabelle/Scala operations);
Wed, 26 Nov 2014 20:05:34 +0100 wenzelm renamed "pairself" to "apply2", in accordance to @{apply 2};
Fri, 11 Apr 2014 11:52:28 +0200 wenzelm explicit 'document_files' in session ROOT specifications;
Thu, 23 Aug 2012 17:46:03 +0200 wenzelm tuned messages: end-of-input rarely means physical end-of-file from the past;
Mon, 23 Jul 2012 15:44:42 +0200 wenzelm removed redundant check (cf. a8ed41b6280b);
Sun, 11 Sep 2011 17:30:01 +0200 wenzelm more orthogonal signature;
Sat, 16 Jul 2011 18:41:35 +0200 wenzelm some file and directory operations;
Sat, 16 Jul 2011 17:11:49 +0200 wenzelm added File.fold_pages for streaming of large files;
Fri, 01 Jul 2011 13:54:25 +0200 noschinl reverted 782991e4180d: fold_fields was never used
Wed, 13 Apr 2011 20:43:00 +0200 noschinl Generalized File.fold_lines to File.fold_fields
Sun, 20 Mar 2011 17:40:45 +0100 wenzelm replaced File.check by specific File.check_file, File.check_dir;
Sun, 13 Mar 2011 16:01:00 +0100 wenzelm Path.print is the official way to show file-system paths to users -- note that Path.implode often indicates violation of the abstract datatype;
Sun, 28 Nov 2010 16:35:56 +0100 wenzelm more permissive Isabelle_System.mkdir;
Sat, 27 Nov 2010 15:58:36 +0100 wenzelm explicit check for requirement;
Sat, 27 Nov 2010 15:36:35 +0100 wenzelm tuned;
Sat, 27 Nov 2010 15:28:00 +0100 wenzelm more explicit Isabelle_System operations;
Sat, 27 Nov 2010 14:19:04 +0100 wenzelm moved file identification to thy_load.ML (where it is actually used);
Thu, 08 Jul 2010 09:36:22 +0200 haftmann rm_tree: remove entire file system trees
Thu, 01 Jul 2010 13:38:17 +0200 haftmann refined semantics of mkdir_leaf: do not fail if directory already exists
Wed, 30 Jun 2010 12:20:45 +0200 haftmann mkdir_leaf -- avoiding surprises with typos in user-given paths
Sat, 06 Feb 2010 14:50:55 +0100 wenzelm renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
Tue, 27 Oct 2009 13:16:16 +0100 wenzelm non-critical atomic accesses;
Thu, 15 Oct 2009 15:45:50 +0200 wenzelm exported File.shell_quote;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Sat, 27 Jun 2009 17:34:48 +0200 wenzelm builtin isabelle_tool for ML and Scala -- avoids excessive shell script (especially important for Cygwin);
Wed, 21 Jan 2009 23:21:44 +0100 wenzelm removed Ids;
Mon, 06 Oct 2008 22:41:21 +0200 wenzelm fold_lines: more tuning, avoiding extra split_last;
Sat, 04 Oct 2008 16:05:09 +0200 wenzelm replaced ISATOOL by ISABELLE_TOOL;
Sat, 04 Oct 2008 14:29:43 +0200 wenzelm renamed isatool to isabelle_tool in programming interfaces;
Thu, 28 Aug 2008 20:29:40 +0200 wenzelm tuned fold_lines;
Thu, 28 Aug 2008 20:19:45 +0200 wenzelm fold_lines: simplified, more efficient due to String.fields;
Wed, 27 Aug 2008 20:36:27 +0200 wenzelm renamed Buffer.write to File.write_buffer;
less more (0) -100 -60 tip