equal
deleted
inserted
replaced
228 val log_gz = isabelle_output + store.log_gz(session_name) |
228 val log_gz = isabelle_output + store.log_gz(session_name) |
229 |
229 |
230 val properties = |
230 val properties = |
231 if (database.is_file) { |
231 if (database.is_file) { |
232 using(SQLite.open_database(database))(db => |
232 using(SQLite.open_database(database))(db => |
233 store.read_build_log(db, ml_statistics = true)).ml_statistics |
233 store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics |
234 } |
234 } |
235 else if (log_gz.is_file) { |
235 else if (log_gz.is_file) { |
236 Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics |
236 Build_Log.Log_File(log_gz).parse_session_info(ml_statistics = true).ml_statistics |
237 } |
237 } |
238 else Nil |
238 else Nil |