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;
--- 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 */