src/Pure/Admin/build_status.scala
changeset 65838 30c2d78b5d38
parent 65836 3b4877fbd9cb
child 65847 ad35427dbe88
     1.1 --- a/src/Pure/Admin/build_status.scala	Sun May 14 21:56:58 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 14 22:04:52 2017 +0200
     1.3 @@ -203,18 +203,16 @@
     1.4      def clean_name(name: String): String =
     1.5        name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
     1.6  
     1.7 -    HTML.init_dir(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"),
    1.12 -          HTML.par(
    1.13 -            List(HTML.description(
    1.14 -              List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
    1.15 -          HTML.par(
    1.16 -            List(HTML.itemize(data.entries.map({ case data_entry =>
    1.17 -              List(HTML.link(clean_name(data_entry.name) + "/index.html",
    1.18 -                HTML.text(data_entry.name))) })))))))
    1.19 +    HTML.write_document(target_dir, "index.html",
    1.20 +      List(HTML.title("Isabelle build status")),
    1.21 +      List(HTML.chapter("Isabelle build status"),
    1.22 +        HTML.par(
    1.23 +          List(HTML.description(
    1.24 +            List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
    1.25 +        HTML.par(
    1.26 +          List(HTML.itemize(data.entries.map({ case data_entry =>
    1.27 +            List(HTML.link(clean_name(data_entry.name) + "/index.html",
    1.28 +              HTML.text(data_entry.name))) }))))))
    1.29  
    1.30      for (data_entry <- data.entries) {
    1.31        val data_name = data_entry.name
    1.32 @@ -308,37 +306,35 @@
    1.33              }
    1.34            }, data_entry.sessions).toMap
    1.35  
    1.36 -      HTML.init_dir(dir)
    1.37 -      File.write(dir + Path.basic("index.html"),
    1.38 -        HTML.output_document(
    1.39 -          List(HTML.title("Isabelle build status for " + data_name)),
    1.40 -          HTML.chapter("Isabelle build status for " + data_name) ::
    1.41 -          HTML.par(
    1.42 -            List(HTML.description(
    1.43 -              List(
    1.44 -                HTML.text("status date:") -> HTML.text(data.date.toString),
    1.45 -                HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) ::
    1.46 -          HTML.par(
    1.47 -            List(HTML.itemize(
    1.48 -              data_entry.sessions.map(session =>
    1.49 -                HTML.link("#session_" + session.name, HTML.text(session.name)) ::
    1.50 -                HTML.text(" (" + session.timing.message_resources + ")"))))) ::
    1.51 -          data_entry.sessions.flatMap(session =>
    1.52 +      HTML.write_document(dir, "index.html",
    1.53 +        List(HTML.title("Isabelle build status for " + data_name)),
    1.54 +        HTML.chapter("Isabelle build status for " + data_name) ::
    1.55 +        HTML.par(
    1.56 +          List(HTML.description(
    1.57              List(
    1.58 -              HTML.section(session.name) + HTML.id("session_" + session.name),
    1.59 -              HTML.par(
    1.60 -                HTML.description(
    1.61 -                  List(
    1.62 -                    HTML.text("timing:") -> HTML.text(session.timing.message_resources),
    1.63 -                    HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) :::
    1.64 -                  proper_string(session.isabelle_version).map(s =>
    1.65 -                    HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
    1.66 -                  proper_string(session.afp_version).map(s =>
    1.67 -                    HTML.text("AFP version:") -> HTML.text(s)).toList) ::
    1.68 -                session_plots.getOrElse(session.name, Nil).map(plot_name =>
    1.69 -                  HTML.image(plot_name) +
    1.70 -                    HTML.width(image_width / 2) +
    1.71 -                    HTML.height(image_height / 2)))))))
    1.72 +              HTML.text("status date:") -> HTML.text(data.date.toString),
    1.73 +              HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) ::
    1.74 +        HTML.par(
    1.75 +          List(HTML.itemize(
    1.76 +            data_entry.sessions.map(session =>
    1.77 +              HTML.link("#session_" + session.name, HTML.text(session.name)) ::
    1.78 +              HTML.text(" (" + session.timing.message_resources + ")"))))) ::
    1.79 +        data_entry.sessions.flatMap(session =>
    1.80 +          List(
    1.81 +            HTML.section(session.name) + HTML.id("session_" + session.name),
    1.82 +            HTML.par(
    1.83 +              HTML.description(
    1.84 +                List(
    1.85 +                  HTML.text("timing:") -> HTML.text(session.timing.message_resources),
    1.86 +                  HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) :::
    1.87 +                proper_string(session.isabelle_version).map(s =>
    1.88 +                  HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
    1.89 +                proper_string(session.afp_version).map(s =>
    1.90 +                  HTML.text("AFP version:") -> HTML.text(s)).toList) ::
    1.91 +              session_plots.getOrElse(session.name, Nil).map(plot_name =>
    1.92 +                HTML.image(plot_name) +
    1.93 +                  HTML.width(image_width / 2) +
    1.94 +                  HTML.height(image_height / 2))))))
    1.95      }
    1.96    }
    1.97