201 image_size: (Int, Int) = default_image_size) |
201 image_size: (Int, Int) = default_image_size) |
202 { |
202 { |
203 def clean_name(name: String): String = |
203 def clean_name(name: String): String = |
204 name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString) |
204 name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString) |
205 |
205 |
206 HTML.init_dir(target_dir) |
206 HTML.write_document(target_dir, "index.html", |
207 File.write(target_dir + Path.basic("index.html"), |
207 List(HTML.title("Isabelle build status")), |
208 HTML.output_document( |
208 List(HTML.chapter("Isabelle build status"), |
209 List(HTML.title("Isabelle build status")), |
209 HTML.par( |
210 List(HTML.chapter("Isabelle build status"), |
210 List(HTML.description( |
211 HTML.par( |
211 List(HTML.text("status date:") -> HTML.text(data.date.toString))))), |
212 List(HTML.description( |
212 HTML.par( |
213 List(HTML.text("status date:") -> HTML.text(data.date.toString))))), |
213 List(HTML.itemize(data.entries.map({ case data_entry => |
214 HTML.par( |
214 List(HTML.link(clean_name(data_entry.name) + "/index.html", |
215 List(HTML.itemize(data.entries.map({ case data_entry => |
215 HTML.text(data_entry.name))) })))))) |
216 List(HTML.link(clean_name(data_entry.name) + "/index.html", |
|
217 HTML.text(data_entry.name))) }))))))) |
|
218 |
216 |
219 for (data_entry <- data.entries) { |
217 for (data_entry <- data.entries) { |
220 val data_name = data_entry.name |
218 val data_name = data_entry.name |
221 |
219 |
222 val image_width = (image_size._1 * data_entry.stretch).toInt |
220 val image_width = (image_size._1 * data_entry.stretch).toInt |
306 |
304 |
307 session.name -> plot_names |
305 session.name -> plot_names |
308 } |
306 } |
309 }, data_entry.sessions).toMap |
307 }, data_entry.sessions).toMap |
310 |
308 |
311 HTML.init_dir(dir) |
309 HTML.write_document(dir, "index.html", |
312 File.write(dir + Path.basic("index.html"), |
310 List(HTML.title("Isabelle build status for " + data_name)), |
313 HTML.output_document( |
311 HTML.chapter("Isabelle build status for " + data_name) :: |
314 List(HTML.title("Isabelle build status for " + data_name)), |
312 HTML.par( |
315 HTML.chapter("Isabelle build status for " + data_name) :: |
313 List(HTML.description( |
316 HTML.par( |
|
317 List(HTML.description( |
|
318 List( |
|
319 HTML.text("status date:") -> HTML.text(data.date.toString), |
|
320 HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) :: |
|
321 HTML.par( |
|
322 List(HTML.itemize( |
|
323 data_entry.sessions.map(session => |
|
324 HTML.link("#session_" + session.name, HTML.text(session.name)) :: |
|
325 HTML.text(" (" + session.timing.message_resources + ")"))))) :: |
|
326 data_entry.sessions.flatMap(session => |
|
327 List( |
314 List( |
328 HTML.section(session.name) + HTML.id("session_" + session.name), |
315 HTML.text("status date:") -> HTML.text(data.date.toString), |
329 HTML.par( |
316 HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) :: |
330 HTML.description( |
317 HTML.par( |
331 List( |
318 List(HTML.itemize( |
332 HTML.text("timing:") -> HTML.text(session.timing.message_resources), |
319 data_entry.sessions.map(session => |
333 HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) ::: |
320 HTML.link("#session_" + session.name, HTML.text(session.name)) :: |
334 proper_string(session.isabelle_version).map(s => |
321 HTML.text(" (" + session.timing.message_resources + ")"))))) :: |
335 HTML.text("Isabelle version:") -> HTML.text(s)).toList ::: |
322 data_entry.sessions.flatMap(session => |
336 proper_string(session.afp_version).map(s => |
323 List( |
337 HTML.text("AFP version:") -> HTML.text(s)).toList) :: |
324 HTML.section(session.name) + HTML.id("session_" + session.name), |
338 session_plots.getOrElse(session.name, Nil).map(plot_name => |
325 HTML.par( |
339 HTML.image(plot_name) + |
326 HTML.description( |
340 HTML.width(image_width / 2) + |
327 List( |
341 HTML.height(image_height / 2))))))) |
328 HTML.text("timing:") -> HTML.text(session.timing.message_resources), |
|
329 HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) ::: |
|
330 proper_string(session.isabelle_version).map(s => |
|
331 HTML.text("Isabelle version:") -> HTML.text(s)).toList ::: |
|
332 proper_string(session.afp_version).map(s => |
|
333 HTML.text("AFP version:") -> HTML.text(s)).toList) :: |
|
334 session_plots.getOrElse(session.name, Nil).map(plot_name => |
|
335 HTML.image(plot_name) + |
|
336 HTML.width(image_width / 2) + |
|
337 HTML.height(image_height / 2)))))) |
342 } |
338 } |
343 } |
339 } |
344 |
340 |
345 |
341 |
346 /* Isabelle tool wrapper */ |
342 /* Isabelle tool wrapper */ |