--- a/src/Pure/Admin/build_release.scala Sun May 14 21:56:58 2017 +0200
+++ b/src/Pure/Admin/build_release.scala Sun May 14 22:04:52 2017 +0200
@@ -127,16 +127,14 @@
HTML.link("https://bitbucket.org/isa-afp/afp-devel/commits/" + afp_rev,
HTML.text("AFP/" + afp_rev))
- HTML.init_dir(dir)
- File.write(dir + Path.explode("index.html"),
- HTML.output_document(
- List(HTML.title(release_info.name)),
- List(
- HTML.chapter(release_info.name + " (" + release_id + ")"),
- HTML.itemize(
- website_platform_bundles.map({ case (bundle, info) =>
- List(HTML.link(bundle, HTML.text(info.platform_description))) }))) :::
- (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link))))))
+ HTML.write_document(dir, "index.html",
+ List(HTML.title(release_info.name)),
+ List(
+ HTML.chapter(release_info.name + " (" + release_id + ")"),
+ HTML.itemize(
+ website_platform_bundles.map({ case (bundle, info) =>
+ List(HTML.link(bundle, HTML.text(info.platform_description))) }))) :::
+ (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link)))))
for ((bundle, _) <- website_platform_bundles)
File.copy(release_info.dist_dir + Path.explode(bundle), dir)
--- a/src/Pure/Admin/build_status.scala Sun May 14 21:56:58 2017 +0200
+++ b/src/Pure/Admin/build_status.scala Sun May 14 22:04:52 2017 +0200
@@ -203,18 +203,16 @@
def clean_name(name: String): String =
name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
- HTML.init_dir(target_dir)
- File.write(target_dir + Path.basic("index.html"),
- HTML.output_document(
- List(HTML.title("Isabelle build status")),
- List(HTML.chapter("Isabelle build status"),
- HTML.par(
- List(HTML.description(
- List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
- HTML.par(
- List(HTML.itemize(data.entries.map({ case data_entry =>
- List(HTML.link(clean_name(data_entry.name) + "/index.html",
- HTML.text(data_entry.name))) })))))))
+ HTML.write_document(target_dir, "index.html",
+ List(HTML.title("Isabelle build status")),
+ List(HTML.chapter("Isabelle build status"),
+ HTML.par(
+ List(HTML.description(
+ List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
+ HTML.par(
+ List(HTML.itemize(data.entries.map({ case data_entry =>
+ List(HTML.link(clean_name(data_entry.name) + "/index.html",
+ HTML.text(data_entry.name))) }))))))
for (data_entry <- data.entries) {
val data_name = data_entry.name
@@ -308,37 +306,35 @@
}
}, data_entry.sessions).toMap
- HTML.init_dir(dir)
- File.write(dir + Path.basic("index.html"),
- HTML.output_document(
- List(HTML.title("Isabelle build status for " + data_name)),
- HTML.chapter("Isabelle build status for " + data_name) ::
- HTML.par(
- List(HTML.description(
- List(
- HTML.text("status date:") -> HTML.text(data.date.toString),
- HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) ::
- HTML.par(
- List(HTML.itemize(
- data_entry.sessions.map(session =>
- HTML.link("#session_" + session.name, HTML.text(session.name)) ::
- HTML.text(" (" + session.timing.message_resources + ")"))))) ::
- data_entry.sessions.flatMap(session =>
+ HTML.write_document(dir, "index.html",
+ List(HTML.title("Isabelle build status for " + data_name)),
+ HTML.chapter("Isabelle build status for " + data_name) ::
+ HTML.par(
+ List(HTML.description(
List(
- HTML.section(session.name) + HTML.id("session_" + session.name),
- HTML.par(
- HTML.description(
- List(
- HTML.text("timing:") -> HTML.text(session.timing.message_resources),
- HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) :::
- proper_string(session.isabelle_version).map(s =>
- HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
- proper_string(session.afp_version).map(s =>
- HTML.text("AFP version:") -> HTML.text(s)).toList) ::
- session_plots.getOrElse(session.name, Nil).map(plot_name =>
- HTML.image(plot_name) +
- HTML.width(image_width / 2) +
- HTML.height(image_height / 2)))))))
+ HTML.text("status date:") -> HTML.text(data.date.toString),
+ HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) ::
+ HTML.par(
+ List(HTML.itemize(
+ data_entry.sessions.map(session =>
+ HTML.link("#session_" + session.name, HTML.text(session.name)) ::
+ HTML.text(" (" + session.timing.message_resources + ")"))))) ::
+ data_entry.sessions.flatMap(session =>
+ List(
+ HTML.section(session.name) + HTML.id("session_" + session.name),
+ HTML.par(
+ HTML.description(
+ List(
+ HTML.text("timing:") -> HTML.text(session.timing.message_resources),
+ HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) :::
+ proper_string(session.isabelle_version).map(s =>
+ HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
+ proper_string(session.afp_version).map(s =>
+ HTML.text("AFP version:") -> HTML.text(s)).toList) ::
+ session_plots.getOrElse(session.name, Nil).map(plot_name =>
+ HTML.image(plot_name) +
+ HTML.width(image_width / 2) +
+ HTML.height(image_height / 2))))))
}
}
--- a/src/Pure/Admin/isabelle_devel.scala Sun May 14 21:56:58 2017 +0200
+++ b/src/Pure/Admin/isabelle_devel.scala Sun May 14 22:04:52 2017 +0200
@@ -25,27 +25,25 @@
{
val header = "Isabelle Development Resources"
- HTML.init_dir(root)
- File.write(root + Path.explode("index.html"),
- HTML.output_document(
- List(HTML.title(header)),
- List(HTML.chapter(header),
- HTML.itemize(
- List(
- HTML.text("Isabelle nightly ") :::
- List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) :::
- HTML.text(" (for all platforms)"),
+ HTML.write_document(root, "index.html",
+ List(HTML.title(header)),
+ List(HTML.chapter(header),
+ HTML.itemize(
+ List(
+ HTML.text("Isabelle nightly ") :::
+ List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) :::
+ HTML.text(" (for all platforms)"),
- HTML.text("Isabelle ") :::
- List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) :::
- HTML.text(" information"),
+ HTML.text("Isabelle ") :::
+ List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) :::
+ HTML.text(" information"),
- HTML.text("Database with recent ") :::
- List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) :::
- HTML.text(" information (e.g. for ") :::
- List(HTML.link("http://sqlitebrowser.org",
- List(HTML.code(HTML.text("sqlitebrowser"))))) :::
- HTML.text(")"))))))
+ HTML.text("Database with recent ") :::
+ List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) :::
+ HTML.text(" information (e.g. for ") :::
+ List(HTML.link("http://sqlitebrowser.org",
+ List(HTML.code(HTML.text("sqlitebrowser"))))) :::
+ HTML.text(")")))))
}
--- a/src/Pure/Thy/html.scala Sun May 14 21:56:58 2017 +0200
+++ b/src/Pure/Thy/html.scala Sun May 14 22:04:52 2017 +0200
@@ -157,12 +157,22 @@
output(XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head)),
output(XML.elem("body", body))))
+
+ /* document directory */
+
def init_dir(dir: Path)
{
Isabelle_System.mkdirs(dir)
File.copy(Path.explode("~~/etc/isabelle.css"), dir)
}
+ def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
+ css: String = "isabelle.css")
+ {
+ init_dir(dir)
+ File.write(dir + Path.basic(name), output_document(head, body, css))
+ }
+
/* Isabelle document */