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