equal
deleted
inserted
replaced
167 val isabelle_version = res.string(Build_Log.Prop.isabelle_version) |
167 val isabelle_version = res.string(Build_Log.Prop.isabelle_version) |
168 |
168 |
169 val ml_stats = |
169 val ml_stats = |
170 ML_Statistics( |
170 ML_Statistics( |
171 if (ml_statistics) |
171 if (ml_statistics) |
172 store.uncompress_properties(res.bytes(Build_Log.Data.ml_statistics)) |
172 Properties.uncompress(res.bytes(Build_Log.Data.ml_statistics)) |
173 else Nil, heading = session_name + " (Isabelle/ " + isabelle_version + ")") |
173 else Nil, heading = session_name + " (Isabelle/ " + isabelle_version + ")") |
174 |
174 |
175 val entry = |
175 val entry = |
176 Entry( |
176 Entry( |
177 pull_date = res.date(Build_Log.Data.pull_date), |
177 pull_date = res.date(Build_Log.Data.pull_date), |