[m-rev.] diff: java io.file_type fix

[Peter Wang]

Branches: main, 10.04

library/io.m:
        Make Java implementation of `io.file_type' not return `ok(unknown)'
        for non-existent paths. 

diff --git a/library/io.m b/library/io.m
index f6f244a..1a5739f 100644
--- a/library/io.m
+++ b/library/io.m
@@ -3168,8 +3168,12 @@ file_type_implemented :-
         Result = new io.Res_1.Ok_1(ML_file_type_regular());
     } else if (file.isDirectory()) {
         Result = new io.Res_1.Ok_1(ML_file_type_directory());
-    } else {
+    } else if (file.exists()) {
         Result = new io.Res_1.Ok_1(ML_file_type_unknown());
+    } else {
+        Result = io.ML_make_io_res_1_error_file_type(
+            new java.lang.Exception(""No such file or directory""),
+            ""io.file_type failed: "");
     }
 ").
 

--------------------------------------------------------------------------
mercury-reviews mailing list
Post messages to:       mercury-reviews at csse.unimelb.edu.au
Administrative Queries: owner-mercury-reviews at csse.unimelb.edu.au
Subscriptions:          mercury-reviews-request at csse.unimelb.edu.au
--------------------------------------------------------------------------