# HG changeset patch
# User wenzelm
# Date 1693306408 -7200
# Node ID fdfe9b91d96e6061d93de0c6e2718adb9d593a3b
# Parent  b1e0fb71435dee4bc17c14e0653cf34aae4a5a94
misc tuning: support "scalac -source 3.3";

diff -r b1e0fb71435d -r fdfe9b91d96e src/HOL/Tools/ATP/system_on_tptp.scala
--- a/src/HOL/Tools/ATP/system_on_tptp.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/HOL/Tools/ATP/system_on_tptp.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -70,7 +70,7 @@
   object Run_System extends Scala.Fun_Strings("SystemOnTPTP.run_system", thread = true) {
     val here = Scala_Project.here
     def apply(args: List[String]): List[String] = {
-      val List(url, system, problem_path, extra, Value.Int(timeout)) = args
+      val List(url, system, problem_path, extra, Value.Int(timeout)) = args : @unchecked
       val problem = File.read(Path.explode(problem_path))
 
       val res = run_system(Url(url), system, problem, extra = extra, timeout = Time.ms(timeout))
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Admin/build_log.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -201,7 +201,7 @@
     /* inlined text */
 
     def filter(Marker: Protocol_Message.Marker): List[String] =
-      for (Marker(text) <- lines) yield text
+      for (case Marker(text) <- lines) yield text
 
     def find(Marker: Protocol_Message.Marker): Option[String] =
       lines.collectFirst({ case Marker(text) => text })
@@ -1040,13 +1040,13 @@
           Par_List.map[JFile, Exn.Result[Log_File]](
             file => Exn.capture { Log_File(file) }, file_group)
         db.transaction {
-          for (Exn.Res(log_file) <- log_files) {
+          for (case Exn.Res(log_file) <- log_files) {
             progress.echo("Log " + quote(log_file.name), verbose = true)
             try { status.foreach(_.update(log_file)) }
             catch { case exn: Throwable => add_error(log_file.name, exn) }
           }
         }
-        for ((file, Exn.Exn(exn)) <- file_group.zip(log_files)) {
+        for (case (file, Exn.Exn(exn)) <- file_group.zip(log_files)) {
           add_error(Log_File.plain_name(file), exn)
         }
       }
@@ -1071,8 +1071,8 @@
                else
                 res.get_string(c)))
           val n = Prop.all_props.length
-          val props = for ((x, Some(y)) <- results.take(n)) yield (x, y)
-          val settings = for ((x, Some(y)) <- results.drop(n)) yield (x, y)
+          val props = for (case (x, Some(y)) <- results.take(n)) yield (x, y)
+          val settings = for (case (x, Some(y)) <- results.drop(n)) yield (x, y)
           Meta_Info(props, settings)
         }
       )
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Admin/build_release.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -189,7 +189,7 @@
   def get_bundled_components(dir: Path, platform: Platform.Family.Value): (List[String], String) = {
     val Bundled = new Bundled(platform = Some(platform))
     val components =
-      for { Bundled(name) <- Components.Directory(dir).read_components() } yield name
+      for { case Bundled(name) <- Components.Directory(dir).read_components() } yield name
     val jdk_component =
       components.find(_.startsWith("jdk")) getOrElse error("Missing jdk component")
     (components, jdk_component)
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Concurrent/consumer_thread.scala
--- a/src/Pure/Concurrent/consumer_thread.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Concurrent/consumer_thread.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -89,7 +89,7 @@
 
     val (results, cont) = consume(reqs.map(_.arg))
     for {
-      (Some(req), Some(res)) <- reqs.map(Some(_)).zipAll(results.map(Some(_)), None, None)
+      case (Some(req), Some(res)) <- reqs.map(Some(_)).zipAll(results.map(Some(_)), None, None)
     } {
       (req.ack, res) match {
         case (Some(a), _) => a.change(_ => Some(res))
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/General/json_api.scala
--- a/src/Pure/General/json_api.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/General/json_api.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -69,7 +69,7 @@
   sealed case class Links(json: JSON.T) {
     def get_next: Option[Service] =
       for {
-        JSON.Value.String(next) <- JSON.value(json, "next")
+        case JSON.Value.String(next) <- JSON.value(json, "next")
         if Url.is_wellformed(next)
       } yield new Service(Url(next))
 
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/General/mercurial.scala
--- a/src/Pure/General/mercurial.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/General/mercurial.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -100,7 +100,7 @@
 
   sealed case class Archive_Info(lines: List[String]) {
     def id: Option[String] = lines.collectFirst({ case Archive_Node(a) => a })
-    def tags: List[String] = for (Archive_Tag(tag) <- lines if tag != "tip") yield tag
+    def tags: List[String] = for (case Archive_Tag(tag) <- lines if tag != "tip") yield tag
   }
 
   def archive_info(root: Path): Option[Archive_Info] = {
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/General/symbol.scala
--- a/src/Pure/General/symbol.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/General/symbol.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -327,9 +327,10 @@
           case _ => None
         }
 
-      val groups = proper_list(for ((Group.name, a) <- props) yield a).getOrElse(List("unsorted"))
+      val groups =
+        proper_list(for (case (Group.name, a) <- props) yield a).getOrElse(List("unsorted"))
 
-      val abbrevs = for ((Abbrev.name, a) <- props) yield a
+      val abbrevs = for (case (Abbrev.name, a) <- props) yield a
 
       new Entry(symbol, name, argument, code, Font.unapply(props), groups, abbrevs)
     }
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/PIDE/command.scala
--- a/src/Pure/PIDE/command.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/PIDE/command.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -147,13 +147,13 @@
       else other.rep.iterator.foldLeft(this)(_ + _)
 
     def redirection_iterator: Iterator[Document_ID.Generic] =
-      for (Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
+      for (case Markup_Index(_, Symbol.Text_Chunk.Id(id)) <- rep.keysIterator)
         yield id
 
     def redirect(other_id: Document_ID.Generic): Markups = {
       val rep1 =
         (for {
-          (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator
+          case (Markup_Index(status, Symbol.Text_Chunk.Id(id)), markup) <- rep.iterator
           if other_id == id
         } yield (Markup_Index(status, Symbol.Text_Chunk.Default), markup)).toMap
       if (rep1.isEmpty) Markups.empty else new Markups(rep1)
@@ -500,13 +500,13 @@
   def blobs_ok: Boolean = blobs.forall(Exn.the_res.isDefinedAt)
 
   def blobs_names: List[Document.Node.Name] =
-    for (Exn.Res(blob) <- blobs) yield blob.name
+    for (case Exn.Res(blob) <- blobs) yield blob.name
 
   def blobs_undefined: List[Document.Node.Name] =
-    for (Exn.Res(blob) <- blobs if blob.content.isEmpty) yield blob.name
+    for (case Exn.Res(blob) <- blobs if blob.content.isEmpty) yield blob.name
 
   def blobs_defined: List[(Document.Node.Name, SHA1.Digest)] =
-    for (Exn.Res(blob) <- blobs; (digest, _) <- blob.content) yield (blob.name, digest)
+    for (case Exn.Res(blob) <- blobs; (digest, _) <- blob.content) yield (blob.name, digest)
 
   def blobs_changed(doc_blobs: Document.Blobs): Boolean =
     blobs.exists({ case Exn.Res(blob) => doc_blobs.changed(blob.name) case _ => false })
@@ -518,7 +518,7 @@
 
   val chunks: Map[Symbol.Text_Chunk.Name, Symbol.Text_Chunk] =
     ((Symbol.Text_Chunk.Default -> chunk) ::
-      (for (Exn.Res(blob) <- blobs; (_, file) <- blob.content)
+      (for (case Exn.Res(blob) <- blobs; (_, file) <- blob.content)
         yield blob.chunk_file -> file)).toMap
 
   def length: Int = source.length
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/PIDE/document.scala
--- a/src/Pure/PIDE/document.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/PIDE/document.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -785,7 +785,7 @@
             case some => Some(some)
           }
       }
-      for (Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status))
+      for (case Text.Info(r, Some(x)) <- cumulate(range, None, elements, result1, status))
         yield Text.Info(r, x)
     }
   }
@@ -1262,7 +1262,7 @@
       val pending_edits1 =
         (for {
           change <- history.undo_list.takeWhile(_ != stable)
-          (name, Node.Edits(es)) <- change.rev_edits
+          case (name, Node.Edits(es)) <- change.rev_edits
         } yield (name -> es)).foldLeft(pending_edits)(_ + _)
 
       new Snapshot(this, version, node_name, pending_edits1, snippet_command)
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/PIDE/query_operation.scala
--- a/src/Pure/PIDE/query_operation.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/PIDE/query_operation.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -76,7 +76,7 @@
           val command_results = snapshot.command_results(cmd)
           val results =
             (for {
-              (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
+              case (_, elem @ XML.Elem(Markup(Markup.RESULT, props), _)) <- command_results.iterator
               if props.contains((Markup.INSTANCE, state0.instance))
             } yield elem).toList
           val removed = !snapshot.get_node(cmd.node_name).commands.contains(cmd)
@@ -116,7 +116,7 @@
 
     val new_output =
       for {
-        XML.Elem(_, List(XML.Elem(markup, body))) <- results
+        case XML.Elem(_, List(XML.Elem(markup, body))) <- results
         if Markup.messages.contains(markup.name)
         body1 = resolve_sendback(body)
       } yield Protocol.make_message(body1, markup.name, props = markup.properties)
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/PIDE/rendering.scala
--- a/src/Pure/PIDE/rendering.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/PIDE/rendering.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -405,7 +405,7 @@
                 Some(snapshot.convert(info.range))
               else None)
         })
-    for (Text.Info(range, Some(range1)) <- result)
+    for (case Text.Info(range, Some(range1)) <- result)
       yield Text.Info(range, range1)
   }
 
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/System/executable.scala
--- a/src/Pure/System/executable.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/System/executable.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -31,7 +31,7 @@
       if (Platform.is_macos) {
         val Pattern = """^\s*(/.+)\s+\(.*\)$""".r
         for {
-          Pattern(lib) <- ldd_lines
+          case Pattern(lib) <- ldd_lines
           if !lib.startsWith("@executable_path/") && filter(lib_name(lib))
         } yield lib
       }
@@ -42,7 +42,7 @@
             case None => ""
             case Some(path) => path.absolute.implode
           }
-        for { Pattern(lib) <- ldd_lines if filter(lib_name(lib)) }
+        for { case Pattern(lib) <- ldd_lines if filter(lib_name(lib)) }
           yield prefix + lib
       }
 
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -481,7 +481,7 @@
             (entry, result)
           }
         for {
-          (entry, Some(res)) <- items
+          case (entry, Some(res)) <- items
           if !entry.isDirectory
           t <- Option(entry.getLastModifiedTime)
         } Files.setLastModifiedTime(res, t)
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Thy/export.scala
--- a/src/Pure/Thy/export.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Thy/export.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -379,10 +379,10 @@
                 yield name -> store.try_open_database(name, server_mode = false)
             attempts.collectFirst({ case (name, None) => name }) match {
               case Some(bad) =>
-                for ((_, Some(db)) <- attempts) db.close()
+                for (case (_, Some(db)) <- attempts) db.close()
                 store.error_database(bad)
               case None =>
-                for ((name, Some(db)) <- attempts) yield {
+                for (case (name, Some(db)) <- attempts) yield {
                   new Session_Database(name, db) { override def close(): Unit = this.db.close() }
                 }
             }
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Thy/html.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -151,7 +151,7 @@
   def check_control_blocks(body: XML.Body): Boolean = {
     var ok = true
     var open = List.empty[Symbol.Symbol]
-    for { XML.Text(text) <- body; sym <- Symbol.iterator(text) } {
+    for { case XML.Text(text) <- body; sym <- Symbol.iterator(text) } {
       if (is_control_block_begin(sym)) open ::= sym
       else if (is_control_block_end(sym)) {
         open match {
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Tools/build.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -723,7 +723,7 @@
 
       val results =
         Command.Results.make(
-          for (elem @ XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
+          for (case elem@XML.Elem(Markup(_, Markup.Serial(i)), _) <- read_xml(Export.MESSAGES))
             yield i -> elem)
 
       val command =
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Tools/build_cluster.scala
--- a/src/Pure/Tools/build_cluster.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Tools/build_cluster.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -262,7 +262,7 @@
       _sessions
     }
     else {
-      for (Exn.Res(session) <- attempts) session.close()
+      for (case Exn.Res(session) <- attempts) session.close()
       error("Failed to connect build cluster")
     }
   }
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Tools/check_keywords.scala
--- a/src/Pure/Tools/check_keywords.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Tools/check_keywords.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -22,7 +22,7 @@
 
       val result =
         parse_all(rep(item), Token.reader(Token.explode(keywords, input), start)) match {
-          case Success(res, _) => for (Some(x) <- res) yield x
+          case Success(res, _) => for (case Some(x) <- res) yield x
           case bad => error(bad.toString)
         }
     }
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Tools/prismjs.scala
--- a/src/Pure/Tools/prismjs.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Tools/prismjs.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -27,7 +27,7 @@
     val components_json = JSON.parse(File.read(components_path))
     JSON.value(components_json, "languages") match {
       case Some(JSON.Object(langs)) =>
-        (for ((name, JSON.Object(info)) <- langs.iterator if name != "meta") yield {
+        (for (case (name, JSON.Object(info)) <- langs.iterator if name != "meta") yield {
           val alias =
             JSON.Value.List.unapply(info.getOrElse("alias", Nil), JSON.Value.String.unapply)
               .getOrElse(Nil)
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Tools/profiling_report.scala
--- a/src/Pure/Tools/profiling_report.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Tools/profiling_report.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -30,7 +30,7 @@
               thy <- used_theories.iterator
               if theories.isEmpty || theories.contains(thy)
               snapshot <- Build.read_theory(session_context.theory(thy)).iterator
-              (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
+              case (Protocol.ML_Profiling(report), _) <- snapshot.messages.iterator
             } yield if (clean_name) report.clean_name else report).toList
 
           for (report <- ML_Profiling.account(reports)) progress.echo(report.print)
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Tools/simplifier_trace.scala
--- a/src/Pure/Tools/simplifier_trace.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Tools/simplifier_trace.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -208,7 +208,7 @@
                       def purge(queue: Vector[Long]): Unit =
                         queue match {
                           case s +: rest =>
-                            for (Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s))
+                            for (case Item(Markup.SIMP_TRACE_STEP, data) <- results.get(s))
                               memory -= Index.of_data(data)
                             val children = memory_children.getOrElse(s, Set.empty)
                             memory_children -= s
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Tools/spell_checker.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -129,7 +129,7 @@
     val permanent_updates =
       if (dictionary.user_path.is_file)
         for {
-          Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
+          case Spell_Checker.Decl(word, include) <- split_lines(File.read(dictionary.user_path))
         } yield (word, Spell_Checker.Update(include, true))
       else Nil
 
diff -r b1e0fb71435d -r fdfe9b91d96e src/Pure/Tools/task_statistics.scala
--- a/src/Pure/Tools/task_statistics.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Pure/Tools/task_statistics.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -29,7 +29,7 @@
 
   def chart(bins: Int = 100): JFreeChart = {
     val values = new Array[Double](task_statistics.length)
-    for ((Run(x), i) <- task_statistics.iterator.zipWithIndex)
+    for (case (Run(x), i) <- task_statistics.iterator.zipWithIndex)
       values(i) = java.lang.Math.log10((x max 1).toDouble / 1000000)
 
     val data = new HistogramDataset
diff -r b1e0fb71435d -r fdfe9b91d96e src/Tools/Graphview/layout.scala
--- a/src/Tools/Graphview/layout.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Tools/Graphview/layout.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -400,13 +400,13 @@
     output_graph.get_node(Layout.Node(node))
 
   def nodes_iterator: Iterator[Layout.Info] =
-    for ((_: Layout.Node, (info, _)) <- output_graph.iterator) yield info
+    for (case (_: Layout.Node, (info, _)) <- output_graph.iterator) yield info
 
 
   /* dummies */
 
   def dummies_iterator: Iterator[Layout.Info] =
-    for ((_: Layout.Dummy, (info, _)) <- output_graph.iterator) yield info
+    for (case (_: Layout.Dummy, (info, _)) <- output_graph.iterator) yield info
 
   def dummies_iterator(edge: Graph_Display.Edge): Iterator[Layout.Info] =
     new Iterator[Layout.Info] {
diff -r b1e0fb71435d -r fdfe9b91d96e src/Tools/jEdit/src/document_model.scala
--- a/src/Tools/jEdit/src/document_model.scala	Tue Aug 29 12:04:13 2023 +0200
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Aug 29 12:53:28 2023 +0200
@@ -255,12 +255,12 @@
             val open_nodes =
               (for ((_, model) <- st.buffer_models.iterator) yield model.node_name).toList
             val touched_nodes = model_edits.map(_._1)
-            val pending_nodes = for ((node_name, None) <- purged) yield node_name
+            val pending_nodes = for (case (node_name, None) <- purged) yield node_name
             (open_nodes ::: touched_nodes ::: pending_nodes).map((_, Position.none))
           }
           val retain = PIDE.resources.dependencies(imports).theories.toSet
 
-          for ((node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits)
+          for (case (node_name, Some(edits)) <- purged if !retain(node_name); edit <- edits)
             yield edit
         }
         else Nil