--- a/src/Pure/Tools/build_job.scala Sat Apr 09 11:56:48 2022 +0200
+++ b/src/Pure/Tools/build_job.scala Sat Apr 09 12:02:38 2022 +0200
@@ -463,7 +463,11 @@
val result = {
val theory_timing =
- theory_timings.iterator.map({ case props @ Markup.Name(name) => name -> props }).toMap
+ theory_timings.iterator.map(
+ {
+ case props @ Markup.Name(name) => name -> props
+ case _ => ???
+ }).toMap
val used_theory_timings =
for { (name, _) <- deps(session_name).used_theories }
yield theory_timing.getOrElse(name.theory, Markup.Name(name.theory))