# HG changeset patch
# User wenzelm
# Date 1495827652 -7200
# Node ID 1b297ce1e8aa38cee48954cddd2f93ebb2c11756
# Parent  fde7b5d209d56472fa7d3cf2199cf457d76f5374
unused;

diff -r fde7b5d209d5 -r 1b297ce1e8aa src/Pure/Thy/sessions.scala
--- a/src/Pure/Thy/sessions.scala	Fri May 26 20:52:01 2017 +0200
+++ b/src/Pure/Thy/sessions.scala	Fri May 26 21:40:52 2017 +0200
@@ -857,19 +857,6 @@
     def read_errors(db: SQL.Database, name: String): List[String] =
       Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors))
 
-    def read_build_log(db: SQL.Database, name: String,
-      command_timings: Boolean = false,
-      ml_statistics: Boolean = false,
-      task_statistics: Boolean = false): Build_Log.Session_Info =
-    {
-      Build_Log.Session_Info(
-        session_timing = read_session_timing(db, name),
-        command_timings = if (command_timings) read_command_timings(db, name) else Nil,
-        ml_statistics = if (ml_statistics) read_ml_statistics(db, name) else Nil,
-        task_statistics = if (task_statistics) read_task_statistics(db, name) else Nil,
-        errors = read_errors(db, name).map(Library.decode_lines(_)))
-    }
-
     def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
       db.using_statement(Session_Info.table.select(Session_Info.build_columns,
         Session_Info.session_name.where_equal(name)))(stmt =>