--- 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)
}
)