changeset 75438 | 96293bd077bb |
parent 75425 | b958e053d993 |
child 75440 | 39011d0d2128 |
--- a/src/Pure/Tools/build_job.scala Sat Apr 09 15:33:38 2022 +0200 +++ b/src/Pure/Tools/build_job.scala Sat Apr 09 15:35:27 2022 +0200 @@ -463,10 +463,10 @@ val result = { val theory_timing = - theory_timings.iterator.map( + theory_timings.iterator.flatMap( { - case props @ Markup.Name(name) => name -> props - case _ => ??? + case props @ Markup.Name(name) => Some(name -> props) + case _ => None }).toMap val used_theory_timings = for { (name, _) <- deps(session_name).used_theories }