src/Pure/Admin/build_log.scala
changeset 72753 e8da2cfdfcff
parent 72695 45cd55248ffd
child 72860 64378eaf393d
equal deleted inserted replaced
72752:80ae03520fda 72753:e8da2cfdfcff
   495     object Theory_Timing
   495     object Theory_Timing
   496     {
   496     {
   497       def unapply(line: String): Option[(String, (String, Timing))] =
   497       def unapply(line: String): Option[(String, (String, Timing))] =
   498         Protocol.Theory_Timing_Marker.unapply(line.replace('~', '-')).map(log_file.parse_props)
   498         Protocol.Theory_Timing_Marker.unapply(line.replace('~', '-')).map(log_file.parse_props)
   499         match {
   499         match {
   500           case Some((SESSION_NAME, name) :: props) =>
   500           case Some((SESSION_NAME, session) :: props) =>
   501             (props, props) match {
   501             for (theory <- Markup.Name.unapply(props))
   502               case (Markup.Name(thy), Markup.Timing_Properties(t)) => Some((name, thy -> t))
   502             yield (session, theory -> Markup.Timing_Properties.parse(props))
   503               case _ => None
       
   504             }
       
   505           case _ => None
   503           case _ => None
   506         }
   504         }
   507     }
   505     }
   508 
   506 
   509     var chapter = Map.empty[String, String]
   507     var chapter = Map.empty[String, String]