23 |
23 |
24 def make_index() |
24 def make_index() |
25 { |
25 { |
26 val header = "Isabelle Development Resources" |
26 val header = "Isabelle Development Resources" |
27 |
27 |
28 HTML.init_dir(root) |
28 HTML.write_document(root, "index.html", |
29 File.write(root + Path.explode("index.html"), |
29 List(HTML.title(header)), |
30 HTML.output_document( |
30 List(HTML.chapter(header), |
31 List(HTML.title(header)), |
31 HTML.itemize( |
32 List(HTML.chapter(header), |
32 List( |
33 HTML.itemize( |
33 HTML.text("Isabelle nightly ") ::: |
34 List( |
34 List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) ::: |
35 HTML.text("Isabelle nightly ") ::: |
35 HTML.text(" (for all platforms)"), |
36 List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) ::: |
|
37 HTML.text(" (for all platforms)"), |
|
38 |
36 |
39 HTML.text("Isabelle ") ::: |
37 HTML.text("Isabelle ") ::: |
40 List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) ::: |
38 List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) ::: |
41 HTML.text(" information"), |
39 HTML.text(" information"), |
42 |
40 |
43 HTML.text("Database with recent ") ::: |
41 HTML.text("Database with recent ") ::: |
44 List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) ::: |
42 List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) ::: |
45 HTML.text(" information (e.g. for ") ::: |
43 HTML.text(" information (e.g. for ") ::: |
46 List(HTML.link("http://sqlitebrowser.org", |
44 List(HTML.link("http://sqlitebrowser.org", |
47 List(HTML.code(HTML.text("sqlitebrowser"))))) ::: |
45 List(HTML.code(HTML.text("sqlitebrowser"))))) ::: |
48 HTML.text(")")))))) |
46 HTML.text(")"))))) |
49 } |
47 } |
50 |
48 |
51 |
49 |
52 /* release snapshot */ |
50 /* release snapshot */ |
53 |
51 |