src/Pure/General/json.scala
changeset 75405 b13ab7d11b90
parent 75393 87ebf5a50283
child 75406 85e8b4c2b9a9
--- a/src/Pure/General/json.scala	Mon Apr 04 22:42:12 2022 +0200
+++ b/src/Pure/General/json.scala	Mon Apr 04 23:33:14 2022 +0200
@@ -10,7 +10,7 @@
 
 
 import scala.util.matching.Regex
-import scala.util.parsing.combinator.Parsers
+import scala.util.parsing.combinator
 import scala.util.parsing.combinator.lexical.Scanners
 import scala.util.parsing.input.CharArrayReader.EofCh
 
@@ -124,7 +124,7 @@
 
   /* parser */
 
-  trait Parser extends Parsers {
+  trait Parsers extends combinator.Parsers {
     type Elem = Token
 
     def $$$(name: String): Parser[Token] = elem(name, _.is_keyword(name))
@@ -152,12 +152,12 @@
     }
   }
 
-  object Parser extends Parser
+  object Parsers extends Parsers
 
 
   /* standard format */
 
-  def parse(s: S, strict: Boolean = true): T = Parser.parse(s, strict)
+  def parse(s: S, strict: Boolean = true): T = Parsers.parse(s, strict)
 
   object Format {
     def unapply(s: S): Option[T] =