equal
deleted
inserted
replaced
101 val log_dir = dir + Build_Log.log_subdir(date) |
101 val log_dir = dir + Build_Log.log_subdir(date) |
102 val log_path = log_dir + log_filename.ext("xz") |
102 val log_path = log_dir + log_filename.ext("xz") |
103 |
103 |
104 if (!log_path.is_file) { |
104 if (!log_path.is_file) { |
105 progress.echo(log_path.expand.implode) |
105 progress.echo(log_path.expand.implode) |
106 Isabelle_System.mkdirs(log_dir) |
106 Isabelle_System.make_directory(log_dir) |
107 |
107 |
108 val ml_statistics = |
108 val ml_statistics = |
109 session_logs.map(_._1).distinct.sorted.flatMap(session_name => |
109 session_logs.map(_._1).distinct.sorted.flatMap(session_name => |
110 read_ml_statistics(store, session_name). |
110 read_ml_statistics(store, session_name). |
111 map(props => (Build_Log.SESSION_NAME -> session_name) :: props)) |
111 map(props => (Build_Log.SESSION_NAME -> session_name) :: props)) |