equal
deleted
inserted
replaced
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 Isabelle_System.mkdirs(root) |
28 HTML.init_dir(root) |
29 File.write(root + Path.explode("index.html"), |
29 File.write(root + Path.explode("index.html"), |
30 HTML.output_document( |
30 HTML.output_document( |
31 List(HTML.title(header)), |
31 List(HTML.title(header)), |
32 List(HTML.chapter(header), |
32 List(HTML.chapter(header), |
33 HTML.itemize( |
33 HTML.itemize( |