--- a/src/Pure/General/toml.scala Thu Nov 09 14:22:19 2023 +0100
+++ b/src/Pure/General/toml.scala Thu Nov 09 14:28:17 2023 +0100
@@ -423,10 +423,10 @@
object Parse_Context {
case class Seen(inlines: Set[Keys], tables: Set[Keys])
- def empty: Parse_Context = new Parse_Context(Map(Nil -> Seen(Set.empty, Set.empty)))
+ def apply(): Parse_Context = new Parse_Context(Map(Nil -> Seen(Set.empty, Set.empty)))
}
- def parse(s: Str, context: Parse_Context = Parse_Context.empty): Table = {
+ def parse(s: Str, context: Parse_Context = Parse_Context()): Table = {
val file = Parsers.parse(s)
def convert(ks0: Keys, ks1: Keys, v: Parsers.V): T = {