more robust read_file: prefer implicit replacement of bad input instead of failure via MalformedInputException;

--- a/Admin/components/components.sha1	Thu Oct 20 17:05:06 2022 +0200
+++ b/Admin/components/components.sha1	Thu Oct 20 20:14:35 2022 +0200
@@ -158,6 +158,7 @@
 056979bd1c08eb9d0d12cc1118b4ff70bfe2d594 isabelle_setup-20220701.tar.gz
 be91402b3e5ef5bc6d4802a45175ee238cd9653e isabelle_setup-20220808.tar.gz
 171df3eb58bdac4cc495f773b797fa578f7d4be6 isabelle_setup-20220817.tar.gz
+7b1ce9bd85e33076fa7022eeb66ce15915d078d9 isabelle_setup-20221020.tar.gz
 0b2206f914336dec4923dd0479d8cee4b904f544 jdk-11+28.tar.gz
 e12574d838ed55ef2845acf1152329572ab0cc56 jdk-11.0.10+9.tar.gz
 3e05213cad47dbef52804fe329395db9b4e57f39 jdk-11.0.2+9.tar.gz

--- a/Admin/components/main	Thu Oct 20 17:05:06 2022 +0200
+++ b/Admin/components/main	Thu Oct 20 20:14:35 2022 +0200
@@ -9,7 +9,7 @@
 flatlaf-2.4
 idea-icons-20210508
 isabelle_fonts-20211004
-isabelle_setup-20220817
+isabelle_setup-20221020
 jdk-17.0.4.1+1
 jedit-20211103
 jfreechart-1.5.3

--- a/src/Tools/Setup/src/Environment.java	Thu Oct 20 17:05:06 2022 +0200
+++ b/src/Tools/Setup/src/Environment.java	Thu Oct 20 20:14:35 2022 +0200
@@ -9,6 +9,7 @@
 
 import java.io.File;
 import java.io.IOException;
+import java.nio.charset.StandardCharsets;
 import java.nio.file.Files;
 import java.nio.file.Path;
 import java.util.HashMap;
@@ -179,6 +180,11 @@
 
     /* raw process */
 
+    private static read_file(path: Path): String =
+    {
+        return new String(Files.readAllBytes(path), StandardCharsets.UTF_8);
+    }
+
     public static ProcessBuilder process_builder(
         List<String> cmd, File cwd, Map<String,String> env, boolean redirect)
     {
@@ -242,8 +248,8 @@
             }
 
             int rc = proc.exitValue();
-            String out = Files.readString(out_file);
-            String err = Files.readString(err_file);
+            String out = read_file(out_file);
+            String err = read_file(err_file);
             res = new Exec_Result(rc, out, err);
         }
         finally {
@@ -388,7 +394,7 @@
                 Exec_Result res = exec_process(cmd, null, env, true);
                 if (!res.ok()) throw new RuntimeException(res.out());
 
-                for (String s : Files.readString(settings_file).split("\u0000", -1)) {
+                for (String s : read_file(settings_file).split("\u0000", -1)) {
                     int i = s.indexOf('=');
                     if (i > 0) { settings.put(s.substring(0, i), s.substring(i + 1)); }
                     else if (i < 0 && !s.isEmpty()) { settings.put(s, ""); }