# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700145394 -3600
# Node ID a80ee3c97aae6b83d59acfe3f3e92f65fb10c095
# Parent  d5ce982ae60f4782d94dd5b0373b4cd2d672acf3
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;

diff -r d5ce982ae60f -r a80ee3c97aae 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 */