# HG changeset patch # User wenzelm # Date 1606567786 -3600 # Node ID e8da2cfdfcff13630348a348c0efcbe3b3e83d5d # Parent 80ae03520fdaa2210450ec226e1c7175fc21f7b0 more robust (amending a4d7da18ac5c); diff -r 80ae03520fda -r e8da2cfdfcff src/Pure/Admin/build_log.scala --- a/src/Pure/Admin/build_log.scala Sat Nov 28 09:58:56 2020 +0000 +++ b/src/Pure/Admin/build_log.scala Sat Nov 28 13:49:46 2020 +0100 @@ -497,11 +497,9 @@ def unapply(line: String): Option[(String, (String, Timing))] = Protocol.Theory_Timing_Marker.unapply(line.replace('~', '-')).map(log_file.parse_props) match { - case Some((SESSION_NAME, name) :: props) => - (props, props) match { - case (Markup.Name(thy), Markup.Timing_Properties(t)) => Some((name, thy -> t)) - case _ => None - } + case Some((SESSION_NAME, session) :: props) => + for (theory <- Markup.Name.unapply(props)) + yield (session, theory -> Markup.Timing_Properties.parse(props)) case _ => None } }