# HG changeset patch
# User wenzelm
# Date 1495021830 -7200
# Node ID 6ba2dc4552cace4fbddd5e99858a1f6014fa0ffc
# Parent  c103358a55594b0ad92a4b89c5a8ee29bbb3e941
eliminated unused operations;

diff -r c103358a5559 -r 6ba2dc4552ca src/Pure/Admin/build_log.scala
--- a/src/Pure/Admin/build_log.scala	Wed May 17 13:47:19 2017 +0200
+++ b/src/Pure/Admin/build_log.scala	Wed May 17 13:50:30 2017 +0200
@@ -474,21 +474,8 @@
 
   sealed case class Build_Info(sessions: Map[String, Session_Entry])
   {
-    def session(name: String): Session_Entry = sessions(name)
-    def get_session(name: String): Option[Session_Entry] = sessions.get(name)
-
-    def get_default[A](name: String, f: Session_Entry => A, x: A): A =
-      get_session(name) match {
-        case Some(entry) => f(entry)
-        case None => x
-      }
-
-    def finished_sessions: List[String] = sessions.keySet.iterator.filter(finished(_)).toList
-    def finished(name: String): Boolean = get_default(name, _.finished, false)
-    def timing(name: String): Timing = get_default(name, _.timing, Timing.zero)
-    def ml_timing(name: String): Timing = get_default(name, _.ml_timing, Timing.zero)
-    def ml_statistics(name: String): ML_Statistics =
-      get_default(name, entry => ML_Statistics(entry.ml_statistics, name), ML_Statistics.empty)
+    def finished_sessions: List[String] =
+      for ((name, entry) <- sessions.toList if entry.finished) yield name
   }
 
   private def parse_build_info(log_file: Log_File, parse_ml_statistics: Boolean): Build_Info =