properly concatenate toml files: regular toml rules still apply (e.g., inline values may not be changed), but values defined in one file may be updated in another;
authorFabian Huch <huch@in.tum.de>
Thu, 16 Nov 2023 15:36:34 +0100
changeset 78980 a80ee3c97aae
parent 78979 d5ce982ae60f
child 78981 47f8533c6887
properly concatenate toml files: regular toml rules still apply (e.g., inline values may not be changed), but values defined in one file may be updated in another;
src/Pure/General/toml.scala
--- a/src/Pure/General/toml.scala	Thu Nov 16 15:23:41 2023 +0100
+++ b/src/Pure/General/toml.scala	Thu Nov 16 15:36:34 2023 +0100
@@ -529,11 +529,8 @@
     }
   }
 
-  def parse_files(files: Iterable[Path], context: Parse_Context = Parse_Context()): Table = {
-    // FIXME proper reset of table context for each file
-    val s = files.iterator.map(File.read).mkString("\n\n")
-    parse(s, context = context)
-  }
+  def parse_files(files: Iterable[Path], context: Parse_Context = Parse_Context()): Table =
+    files.map(File.read).map(parse(_, context)).foldLeft(Table())(_ ++ _)
 
 
   /* Format TOML */