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