diff -r 7ea69c26524b -r e3af424fdd1a src/Pure/General/properties.scala
--- a/src/Pure/General/properties.scala	Fri Jul 05 00:12:32 2024 +0200
+++ b/src/Pure/General/properties.scala	Fri Jul 05 00:18:51 2024 +0200
@@ -21,6 +21,9 @@
       val i = str.indexOf('=')
       if (i <= 0) None else Some((str.substring(0, i), str.substring(i + 1)))
     }
+
+    def parse(s: java.lang.String): Entry =
+      unapply(s) getOrElse error("Bad property entry: " + quote(s))
   }
 
   def defined(props: T, name: java.lang.String): java.lang.Boolean =