# HG changeset patch
# User wenzelm
# Date 1621256497 -7200
# Node ID 2f4cb9cb087ff887649115a030f6d6d16be16512
# Parent  00ef0f401a29221ac3ddc564fab3ae54dccb38f4
tuned --- clarified corner cases;

diff -r 00ef0f401a29 -r 2f4cb9cb087f src/Pure/System/isabelle_system.scala
--- 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 }