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

[Julien Fischer]

On Thu, 25 Aug 2022, Peter Wang wrote:

> On Wed, 24 Aug 2022 19:16:28 +1000 Julien Fischer <jfischer at opturion.com> wrote:

>>> 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.)
>
> README.Java says we require Java SE 8. Does that mean we can start using nio?

Yes, we can use nio.  (Requiring Java > 8 is off the table for now
however.)

Julien.