# HG changeset patch
# User wenzelm
# Date 1649107994 -7200
# Node ID b13ab7d11b902e8f0dcb7185fb5a35d0389807d9
# Parent  a1363da718aa808efa6a317ae410bd530ca1488c
clarified signature: avoid ambiguity in scala3;

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] =
diff -r a1363da718aa -r b13ab7d11b90 src/Pure/Isar/parse.scala
--- a/src/Pure/Isar/parse.scala	Mon Apr 04 22:42:12 2022 +0200
+++ b/src/Pure/Isar/parse.scala	Mon Apr 04 23:33:14 2022 +0200
@@ -7,14 +7,14 @@
 package isabelle
 
 
-import scala.util.parsing.combinator.Parsers
+import scala.util.parsing.combinator
 import scala.annotation.tailrec
 
 
 object Parse {
   /* parsing tokens */
 
-  trait Parser extends Parsers {
+  trait Parsers extends combinator.Parsers {
     type Elem = Token
 
     def filter_proper: Boolean = true
diff -r a1363da718aa -r b13ab7d11b90 src/Pure/System/options.scala
--- a/src/Pure/System/options.scala	Mon Apr 04 22:42:12 2022 +0200
+++ b/src/Pure/System/options.scala	Mon Apr 04 23:33:14 2022 +0200
@@ -84,7 +84,7 @@
 
   val prefs_syntax: Outer_Syntax = Outer_Syntax.empty + "="
 
-  trait Parser extends Parse.Parser {
+  trait Parsers extends Parse.Parsers {
     val option_name: Parser[String] = atom("option name", _.is_name)
     val option_type: Parser[String] = atom("option type", _.is_name)
     val option_value: Parser[String] =
@@ -95,7 +95,7 @@
       $$$("(") ~! $$$(STANDARD) ~ opt(option_value) ~ $$$(")") ^^ { case _ ~ _ ~ a ~ _ => a }
   }
 
-  private object Parser extends Parser {
+  private object Parsers extends Parsers {
     def comment_marker: Parser[String] =
       $$$("--") | $$$(Symbol.comment) | $$$(Symbol.comment_decoded)
 
@@ -143,8 +143,8 @@
     for {
       dir <- Components.directories()
       file = dir + OPTIONS if file.is_file
-    } { options = Parser.parse_file(options, file.implode, File.read(file)) }
-    opts.foldLeft(Options.Parser.parse_prefs(options, prefs))(_ + _)
+    } { options = Parsers.parse_file(options, file.implode, File.read(file)) }
+    opts.foldLeft(Parsers.parse_prefs(options, prefs))(_ + _)
   }
 
 
diff -r a1363da718aa -r b13ab7d11b90 src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Mon Apr 04 22:42:12 2022 +0200
+++ b/src/Pure/Thy/sessions.scala	Mon Apr 04 23:33:14 2022 +0200
@@ -898,7 +898,7 @@
       document_theories.map(_._1)
   }
 
-  private object Parser extends Options.Parser {
+  private object Parsers extends Options.Parsers {
     private val chapter: Parser[Chapter] = {
       val chapter_name = atom("chapter name", _.is_name)
 
@@ -963,10 +963,10 @@
     }
   }
 
-  def parse_root(path: Path): List[Entry] = Parser.parse_root(path)
+  def parse_root(path: Path): List[Entry] = Parsers.parse_root(path)
 
   def parse_root_entries(path: Path): List[Session_Entry] =
-    for (entry <- Parser.parse_root(path) if entry.isInstanceOf[Session_Entry])
+    for (entry <- Parsers.parse_root(path) if entry.isInstanceOf[Session_Entry])
     yield entry.asInstanceOf[Session_Entry]
 
   def read_root(options: Options, select: Boolean, path: Path): List[Info] = {
diff -r a1363da718aa -r b13ab7d11b90 src/Pure/Thy/thy_element.scala
--- a/src/Pure/Thy/thy_element.scala	Mon Apr 04 22:42:12 2022 +0200
+++ b/src/Pure/Thy/thy_element.scala	Mon Apr 04 23:33:14 2022 +0200
@@ -6,7 +6,7 @@
 
 package isabelle
 
-import scala.util.parsing.combinator.Parsers
+import scala.util.parsing.combinator
 import scala.util.parsing.input
 
 
@@ -58,7 +58,7 @@
       def atEnd: Boolean = in.isEmpty
     }
 
-    object Parser extends Parsers {
+    object Parsers extends combinator.Parsers {
       type Elem = Command
 
       def command(pred: Command => Boolean): Parser[Command] =
@@ -92,6 +92,6 @@
           case bad => error(bad.toString)
         }
     }
-    Parser.apply
+    Parsers.apply
   }
 }
diff -r a1363da718aa -r b13ab7d11b90 src/Pure/Thy/thy_header.scala
--- a/src/Pure/Thy/thy_header.scala	Mon Apr 04 22:42:12 2022 +0200
+++ b/src/Pure/Thy/thy_header.scala	Mon Apr 04 23:33:14 2022 +0200
@@ -123,7 +123,7 @@
 
   /* parser */
 
-  trait Parser extends Parse.Parser {
+  trait Parsers extends Parse.Parsers {
     val header: Parser[Thy_Header] = {
       val load_command =
         ($$$("(") ~! (position(name) <~ $$$(")")) ^^ { case _ ~ x => x }) |
@@ -199,7 +199,7 @@
     (drop_tokens, tokens1 ::: tokens2)
   }
 
-  private object Parser extends Parser {
+  private object Parsers extends Parsers {
     def parse_header(tokens: List[Token], pos: Token.Pos): Thy_Header =
       parse(commit(header), Token.reader(tokens, pos)) match {
         case Success(result, _) => result
@@ -219,7 +219,7 @@
       if (command) Token.Pos.command
       else skip_tokens.foldLeft(Token.Pos.file(node_name.node))(_ advance _)
 
-    Parser.parse_header(tokens, pos).map(Symbol.decode).check(node_name)
+    Parsers.parse_header(tokens, pos).map(Symbol.decode).check(node_name)
   }
 }
 
diff -r a1363da718aa -r b13ab7d11b90 src/Pure/Tools/check_keywords.scala
--- a/src/Pure/Tools/check_keywords.scala	Mon Apr 04 22:42:12 2022 +0200
+++ b/src/Pure/Tools/check_keywords.scala	Mon Apr 04 23:33:14 2022 +0200
@@ -14,7 +14,7 @@
     input: CharSequence,
     start: Token.Pos
   ): List[(Token, Position.T)] = {
-    object Parser extends Parse.Parser {
+    object Parsers extends Parse.Parsers {
       private val conflict =
         position(token("token", tok => !(tok.is_command || tok.is_keyword) && check(tok.source)))
       private val other = token("token", _ => true)
@@ -26,7 +26,7 @@
           case bad => error(bad.toString)
         }
     }
-    Parser.result
+    Parsers.result
   }
 
   def check_keywords(