[m-rev.] for review use the Java library file copying methods

[Zoltan Somogyi]

On 2024-01-08 16:50 +11:00 AEDT, "Julien Fischer" <jfischer at opturion.com> wrote:
> Use the Java library file copying methods.

... in Java grades.

> Use the file copy methods from the Java library when the compiler is built
> in the Java grades.
> 
> compiler/copy_util.m:
>     Add a copy method that use the Files.copy() from the Java library.

s/use the/uses/

The rest is fine, except possibly

> +:- pragma foreign_proc("Java",
> +    do_java_copy_file(Src::in, Dst::in, Error::out, _IO0::di, _IO::uo),
> +    [will_not_call_mercury, promise_pure, thread_safe],
> +"
> +    try {
> +        java.nio.file.Files.copy(
> +            java.nio.file.Paths.get(Src),
> +            java.nio.file.Paths.get(Dst),
> +            java.nio.file.StandardCopyOption.REPLACE_EXISTING,
> +            java.nio.file.StandardCopyOption.COPY_ATTRIBUTES);
> +            Error = null;
> +    } catch (java.lang.Exception e) {
> +        Error = e;
> +    }
> +").

which I don't know enough Java to check.

Zoltan.