# HG changeset patch
# User wenzelm
# Date 1711445441 -3600
# Node ID 98384596b54b20db509e80535512ea1572352dd1
# Parent  e94a36467f4ee4be5da1eeabc206c7543903ca48
clarified meaning of platform.props: update on default;

diff -r e94a36467f4e -r 98384596b54b src/Pure/System/components.scala
--- a/src/Pure/System/components.scala	Mon Mar 25 21:04:26 2024 +0100
+++ b/src/Pure/System/components.scala	Tue Mar 26 10:30:41 2024 +0100
@@ -38,6 +38,7 @@
   /* platforms */
 
   sealed case class Platforms(family_platforms: Map[String, List[Path]]) {
+    def + (entry: (String, List[Path])): Platforms = Platforms(family_platforms + entry)
     def defined(family: String): Boolean = family_platforms.isDefinedAt(family)
     def apply(family: String): List[Path] = family_platforms.getOrElse(family, Nil)
     def path_iterator: Iterator[Path] = family_platforms.valuesIterator.flatten
@@ -210,24 +211,21 @@
 
     def get_platforms(): Platforms = {
       val props_path = platform_props.expand
-      if (props_path.is_file) {
-        val family_platforms =
+      val props =
+        if (props_path.is_file) {
           try {
-            Map.from(
-              for (case (a, b) <- File.read_props(props_path).asScala.iterator)
-                yield {
-                  if (!default_platforms.defined(a)) error("Bad platform family " + quote(a))
-                  val ps = List.from(b.split("\\s+").iterator.filter(_.nonEmpty)).map(Path.explode)
-                  for (p <- ps if !p.all_basic) error("Bad path outside component " + p)
-                  a -> ps
-                })
+            for (case (a, b) <- File.read_props(props_path).asScala.toList)
+              yield {
+                if (!default_platforms.defined(a)) error("Bad platform family " + quote(a))
+                val ps = List.from(b.split("\\s+").iterator.filter(_.nonEmpty)).map(Path.explode)
+                for (p <- ps if !p.all_basic) error("Bad path outside component " + p)
+                a -> ps
+              }
           }
-          catch {
-            case ERROR(msg) => error(msg + Position.here(Position.File(props_path.implode)))
-          }
-        Platforms(family_platforms)
-      }
-      else default_platforms
+          catch { case ERROR(msg) => error(msg + Position.here(Position.File(props_path.implode))) }
+        }
+        else Nil
+      props.foldLeft(default_platforms)(_ + _)
     }
 
     def clean(