# HG changeset patch # User wenzelm # Date 1666289675 -7200 # Node ID ea79c21bcc4733019bb94308e67f8f05d724ebec # Parent adb3f8d33838e73e5ee8a253c3cff8df21bdd7ef more robust read_file: prefer implicit replacement of bad input instead of failure via MalformedInputException; diff -r adb3f8d33838 -r ea79c21bcc47 Admin/components/components.sha1 --- 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 diff -r adb3f8d33838 -r ea79c21bcc47 Admin/components/main --- 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 diff -r adb3f8d33838 -r ea79c21bcc47 src/Tools/Setup/src/Environment.java --- 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 cmd, File cwd, Map 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, ""); }