# HG changeset patch
# User Fabian Huch <huch@in.tum.de>
# Date 1700228315 -3600
# Node ID 8f5be65a176bae5793b0a9e77759c8d0f8db8af3
# Parent  769e850bb1d70884b4942c24439f6f4d9db31933
clarified toml parser interface;

diff -r 769e850bb1d7 -r 8f5be65a176b src/Pure/General/toml.scala
--- a/src/Pure/General/toml.scala	Sun Nov 19 20:45:09 2023 +0100
+++ b/src/Pure/General/toml.scala	Fri Nov 17 14:38:35 2023 +0100
@@ -402,12 +402,6 @@
 
     private def content: Parser[List[(Keys, V)]] =
       rep((key <~! $$$("=")) ~! toml_value <~! line_sep ^^ { case ks ~ v => ks -> v })
-
-
-    /* parse */
-
-    def parse(input: Str): ParseResult[File] =
-      phrase(toml)(new Lexer.Scanner(Scan.char_reader(input + EofCh)))
   }
 
   object Parsers extends Parsers
@@ -483,7 +477,7 @@
 
   def parse(s: Str, context: Parse_Context = Parse_Context()): Table = {
     val file =
-      Parsers.parse(s) match {
+      Parsers.phrase(Parsers.toml)(new Lexer.Scanner(Scan.char_reader(s + EofCh))) match {
         case Parsers.Success (toml, _) => toml
         case Parsers.Error(msg, next) => context.error("Error parsing toml: " + msg, next.pos)
         case Parsers.Failure (msg, next) =>