| Tue, 03 Jan 2023 16:05:07 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 24 Jun 2022 23:38:41 +0200 |
wenzelm |
clarified signature: File.read_lines is based on scalable Bytes.T;
|
file |
diff |
annotate
|
| Fri, 24 Jun 2022 23:31:28 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Fri, 24 Jun 2022 11:20:14 +0200 |
wenzelm |
unused;
|
file |
diff |
annotate
|
| Thu, 23 Jun 2022 21:50:32 +0200 |
wenzelm |
more scalable generated files and code export, using Bytes.T;
|
file |
diff |
annotate
|
| Wed, 22 Jun 2022 16:25:22 +0200 |
wenzelm |
removed unused operations;
|
file |
diff |
annotate
|
| Wed, 22 Jun 2022 14:31:18 +0200 |
wenzelm |
tuned;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2022 14:51:17 +0200 |
wenzelm |
tuned signature: more operations;
|
file |
diff |
annotate
|
| Tue, 21 Jun 2022 14:22:34 +0200 |
wenzelm |
tuned signature;
|
file |
diff |
annotate
|
| Mon, 20 Jun 2022 16:15:07 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| 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);
|
file |
diff |
annotate
|
| Sat, 20 Feb 2021 23:01:35 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Tue, 27 Oct 2020 22:34:37 +0100 |
wenzelm |
clarified signature: overloaded "+" for Path.append;
|
file |
diff |
annotate
|
| Sun, 20 Sep 2020 20:47:59 +0200 |
wenzelm |
clarified signature;
|
file |
diff |
annotate
|
| Sat, 02 Nov 2019 13:37:15 +0100 |
wenzelm |
back to more elementary Buffer.T -- less intermediate garbage;
|
file |
diff |
annotate
|
| Mon, 27 May 2019 14:25:00 +0200 |
wenzelm |
tuned whitespace;
|
file |
diff |
annotate
|
| Wed, 19 Dec 2018 21:38:57 +0100 |
wenzelm |
more robust open/close bracket, but with potential danger of blocking indefinitely in uninterruptible state;
|
file |
diff |
annotate
|
| Sat, 08 Dec 2018 21:13:47 +0100 |
wenzelm |
clarified operations: uniform sorting of results;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Sat, 03 Nov 2018 19:31:15 +0100 |
wenzelm |
more operations;
|
file |
diff |
annotate
|
| Thu, 29 Dec 2016 14:43:25 +0100 |
wenzelm |
tuned comments;
|
file |
diff |
annotate
|
| Tue, 18 Oct 2016 16:03:30 +0200 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 11 Aug 2016 18:26:16 +0200 |
wenzelm |
tuned error;
|
file |
diff |
annotate
|
| Mon, 04 Apr 2016 20:45:54 +0200 |
wenzelm |
allow empty string;
|
file |
diff |
annotate
|
| Mon, 07 Mar 2016 21:53:21 +0100 |
wenzelm |
discontinued cd, pwd;
|
file |
diff |
annotate
|
| 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;
|
file |
diff |
annotate
|
| Mon, 29 Feb 2016 15:39:17 +0100 |
wenzelm |
clarified modules;
|
file |
diff |
annotate
|
| Thu, 20 Aug 2015 13:41:53 +0200 |
wenzelm |
precise BinIO, without newline conversion on Windows;
|
file |
diff |
annotate
|
| Tue, 18 Aug 2015 16:08:47 +0200 |
wenzelm |
clarified File.standard_path vs. File.platform_path (like Isabelle/Scala operations);
|
file |
diff |
annotate
|
| Wed, 26 Nov 2014 20:05:34 +0100 |
wenzelm |
renamed "pairself" to "apply2", in accordance to @{apply 2};
|
file |
diff |
annotate
|