50 HTML.write_document(dir, "index.html", |
50 HTML.write_document(dir, "index.html", |
51 List(HTML.title(title + " (" + Distribution.version + ")")), |
51 List(HTML.title(title + " (" + Distribution.version + ")")), |
52 HTML.chapter(title) :: |
52 HTML.chapter(title) :: |
53 (if (sessions.isEmpty) Nil |
53 (if (sessions.isEmpty) Nil |
54 else |
54 else |
55 List(HTML.css_class("sessions")(HTML.div(List( |
55 List(HTML.div("sessions", |
56 HTML.description( |
56 List(HTML.description( |
57 sessions.map({ case (name, description) => |
57 sessions.map({ case (name, description) => |
58 (List(HTML.link(name + "/index.html", HTML.text(name))), |
58 (List(HTML.link(name + "/index.html", HTML.text(name))), |
59 if (description == "") Nil |
59 if (description == "") Nil |
60 else List(HTML.pre(HTML.text(description)))) })))))))) |
60 else List(HTML.pre(HTML.text(description)))) }))))))) |
61 } |
61 } |
62 |
62 |
63 def make_global_index(browser_info: Path) |
63 def make_global_index(browser_info: Path) |
64 { |
64 { |
65 if (!(browser_info + Path.explode("index.html")).is_file) { |
65 if (!(browser_info + Path.explode("index.html")).is_file) { |