--- a/src/Pure/System/isabelle_system.scala Mon May 17 14:54:03 2021 +0200
+++ b/src/Pure/System/isabelle_system.scala Mon May 17 15:01:37 2021 +0200
@@ -128,11 +128,11 @@
if (rc != 0) error(output)
val entries =
- (for (entry <- space_explode('\u0000', File.read(dump)) if entry != "") yield {
- val i = entry.indexOf('=')
- if (i <= 0) entry -> ""
- else entry.substring(0, i) -> entry.substring(i + 1)
- }).toMap
+ space_explode('\u0000', File.read(dump)).flatMap(
+ {
+ case Properties.Eq(a, b) => Some(a -> b)
+ case s => if (s.isEmpty || s.startsWith("=")) None else Some(s -> "")
+ }).toMap
entries + ("PATH" -> entries("PATH_JVM")) - "PATH_JVM"
}
finally { dump.delete }