equal
deleted
inserted
replaced
82 |
82 |
83 get_log("db") match { |
83 get_log("db") match { |
84 case Some(url) => |
84 case Some(url) => |
85 Isabelle_System.with_tmp_file(session_name, "db") { database => |
85 Isabelle_System.with_tmp_file(session_name, "db") { database => |
86 Bytes.write(database, Bytes.read(url)) |
86 Bytes.write(database, Bytes.read(url)) |
87 using(SQLite.open_database(database))(db => |
87 using(SQLite.open_database(database))(db => store.read_ml_statistics(db, session_name)) |
88 store.read_build_log(db, session_name, ml_statistics = true)).ml_statistics |
|
89 } |
88 } |
90 case None => |
89 case None => |
91 get_log("gz") match { |
90 get_log("gz") match { |
92 case Some(url) => |
91 case Some(url) => |
93 val log_file = Build_Log.Log_File(session_name, Url.read_gzip(url)) |
92 val log_file = Build_Log.Log_File(session_name, Url.read_gzip(url)) |