[m-rev.] for review: Improve io.file.m for Java and C#.

[Julien Fischer]

Hi Peter,

On Wed, 24 Aug 2022, Peter Wang wrote:

Start the log message with:

     Improve io.file.m for Java and C#.

otherwise things will look odd in git log.

> remove_file [C#]:
>    Note down a difference in behaviour.
>
> remove_file [Java]:
>    Change error message to look a bit more conventional
>    (beginning with capital letter).
>
> rename_file [C#]:
>    Don't need to check if the file exists before calling Move().
>
>    Note down differences in behaviour.
>
> rename_file [Java]:
>    Throw FileNotFoundException if the old file does not exist.
>    Adjust error messages.
>
> check_file_accessibility [Java]:
>    Throw FileNotFoundException if the file does not exist.
>
>    Throw IOException if an access check fails.
>
> check_file_accessibility [C#]:
>    Implement more directly using foreign code.
>
>    Call EnumerateFileSystemEntries to check if we can read from a
>    directory, which might be a bit faster than GetFileSystemEntries.
>
>    Don't try to set the last access time to check for write access to
>    a directory. That doesn't always work, e.g. it suggests I can't
>    write to /tmp.
>
>    Throw IOException instead System.Exception.
>
>    Document limitations.
>
> file_modification_time [C#]:
>    Also return file modification time for directories.
>
> file_modification_time [Java]:
>    Code style.
>
> make_temp_file [Java]:
>    Return specific error message if temp file already exists
>    (unlikely).
>
>    Catch all exceptions, not only IOExceptions.
>
> make_temp_directory [C#]:
>    Change error message, which included an unnecessary error code
>    (it would always be FFFFFFFF since mkdir() returns -1 on error).
>
>    Throw more specific exceptions.
>
> make_temp_directory [Java]:
>    Catch exceptions just in case.
> ---
> library/io.file.m | 484 ++++++++++++++++++++--------------------------
> 1 file changed, 209 insertions(+), 275 deletions(-)
>

...

> diff --git a/library/io.file.m b/library/io.file.m
> index 22a01a22f..51427bcd9 100644
> --- a/library/io.file.m
> +++ b/library/io.file.m
> +        // This first test just improves the error message in a common case.
> +        if (!old_file.exists()) {
> +            // java.io.FileNotFoundException is documented as being thrown when
> +            // failing to open a file but I don't see any reason we cannot use
> +            // it in this case. (nio also defines a NoSuchFileException class.)

In principle, there's no reason to avoid stuff from the java.nio
package.  (Of course, since we currently don't really use it in the io module,
grabbing the exceptions from there might look a bit odd.)

> +            Error = new java.io.FileNotFoundException(
> +                ""No such file or directory"");
> +        } else if (old_file.renameTo(new_file)) {
> +            Error = null;
>         } else {
> -            // XXX ERROR: use FileNotFoundException?
> -            Error = new java.io.IOException(""No such file or directory"");
> +            Error = new java.io.IOException(""Error renaming file"");
>         }
>     } catch (java.lang.Exception e) {
>         Error = e;

That looks fine.

Julien.