--- 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))
--- 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)
}
)
--- 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)
--- 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))
--- 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))
--- 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] = {
--- 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)
}
--- 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
--- 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)
--- 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)
--- 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)
}
--- 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
}
--- 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)
--- 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() }
}
}
--- 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 {
--- 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 =
--- 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")
}
}
--- 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)
}
}
--- 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)
--- 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)
--- 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
--- 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
--- 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
--- 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] {
--- 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