src/Pure/General/toml.scala
changeset 78939 218929597048
parent 78927 64f47e86526b
child 78941 bc7b7357f4bc
--- a/src/Pure/General/toml.scala	Fri Nov 10 16:03:52 2023 +0100
+++ b/src/Pure/General/toml.scala	Sat Nov 11 13:31:14 2023 +0100
@@ -507,6 +507,11 @@
     }
   }
 
+  def parse_files(files: Iterable[Path], context: Parse_Context = Parse_Context()): Table = {
+    val s = files.iterator.map(File.read).mkString("\n\n")
+    parse(s, context = context)
+  }
+
 
   /* Format TOML */