unused;
authorwenzelm
Fri May 26 21:40:52 2017 +0200 (2017-05-26)
changeset 659381b297ce1e8aa
parent 65937 fde7b5d209d5
child 65939 9fb044904a4d
unused;
src/Pure/Thy/sessions.scala
     1.1 --- a/src/Pure/Thy/sessions.scala	Fri May 26 20:52:01 2017 +0200
     1.2 +++ b/src/Pure/Thy/sessions.scala	Fri May 26 21:40:52 2017 +0200
     1.3 @@ -857,19 +857,6 @@
     1.4      def read_errors(db: SQL.Database, name: String): List[String] =
     1.5        Build_Log.uncompress_errors(read_bytes(db, name, Session_Info.errors))
     1.6  
     1.7 -    def read_build_log(db: SQL.Database, name: String,
     1.8 -      command_timings: Boolean = false,
     1.9 -      ml_statistics: Boolean = false,
    1.10 -      task_statistics: Boolean = false): Build_Log.Session_Info =
    1.11 -    {
    1.12 -      Build_Log.Session_Info(
    1.13 -        session_timing = read_session_timing(db, name),
    1.14 -        command_timings = if (command_timings) read_command_timings(db, name) else Nil,
    1.15 -        ml_statistics = if (ml_statistics) read_ml_statistics(db, name) else Nil,
    1.16 -        task_statistics = if (task_statistics) read_task_statistics(db, name) else Nil,
    1.17 -        errors = read_errors(db, name).map(Library.decode_lines(_)))
    1.18 -    }
    1.19 -
    1.20      def read_build(db: SQL.Database, name: String): Option[Build.Session_Info] =
    1.21        db.using_statement(Session_Info.table.select(Session_Info.build_columns,
    1.22          Session_Info.session_name.where_equal(name)))(stmt =>