diff -r a1363da718aa -r b13ab7d11b90 src/Pure/General/json.scala --- 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] =