src/Pure/Admin/build_status.scala
changeset 65786 84a0ac8a046e
parent 65785 6107504371fb
child 65791 cf48ef4f4e63
     1.1 --- a/src/Pure/Admin/build_status.scala	Tue May 09 11:21:42 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Tue May 09 11:29:18 2017 +0200
     1.3 @@ -165,10 +165,18 @@
     1.4      target_dir: Path = default_target_dir,
     1.5      image_size: (Int, Int) = default_image_size)
     1.6    {
     1.7 +    Isabelle_System.mkdirs(target_dir)
     1.8 +    File.write(target_dir + Path.basic("index.html"),
     1.9 +      HTML.output_document(
    1.10 +        List(HTML.title("Isabelle build status")),
    1.11 +        List(HTML.chapter("Isabelle build status (" + data.date + ")"),
    1.12 +          HTML.itemize(data.entries.map({ case (data_name, _) =>
    1.13 +            List(HTML.link(clean_name(data_name) + "/index.html", HTML.text(data_name))) })))))
    1.14 +
    1.15      for ((data_name, sessions) <- data.entries) {
    1.16 +      progress.echo("output " + quote(data_name))
    1.17 +
    1.18        val dir = target_dir + Path.basic(clean_name(data_name))
    1.19 -
    1.20 -      progress.echo("output " + quote(data_name))
    1.21        Isabelle_System.mkdirs(dir)
    1.22  
    1.23        val session_plots =
    1.24 @@ -273,13 +281,6 @@
    1.25                      HTML.width(image_size._1 / 2) +
    1.26                      HTML.height(image_size._2 / 2)))))))
    1.27      }
    1.28 -
    1.29 -    File.write(target_dir + Path.basic("index.html"),
    1.30 -      HTML.output_document(
    1.31 -        List(HTML.title("Isabelle build status")),
    1.32 -        List(HTML.chapter("Isabelle build status (" + data.date + ")"),
    1.33 -          HTML.itemize(data.entries.map({ case (data_name, _) =>
    1.34 -            List(HTML.link(clean_name(data_name) + "/index.html", HTML.text(data_name))) })))))
    1.35    }
    1.36  
    1.37