tuned signature;
authorwenzelm
Sun May 14 22:04:52 2017 +0200 (2017-05-14)
changeset 6583830c2d78b5d38
parent 65837 9ee6a8d4499b
child 65839 d081671d4a87
tuned signature;
src/Pure/Admin/build_release.scala
src/Pure/Admin/build_status.scala
src/Pure/Admin/isabelle_devel.scala
src/Pure/Thy/html.scala
     1.1 --- a/src/Pure/Admin/build_release.scala	Sun May 14 21:56:58 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_release.scala	Sun May 14 22:04:52 2017 +0200
     1.3 @@ -127,16 +127,14 @@
     1.4          HTML.link("https://bitbucket.org/isa-afp/afp-devel/commits/" + afp_rev,
     1.5            HTML.text("AFP/" + afp_rev))
     1.6  
     1.7 -      HTML.init_dir(dir)
     1.8 -      File.write(dir + Path.explode("index.html"),
     1.9 -        HTML.output_document(
    1.10 -          List(HTML.title(release_info.name)),
    1.11 -          List(
    1.12 -            HTML.chapter(release_info.name + " (" + release_id + ")"),
    1.13 -            HTML.itemize(
    1.14 -              website_platform_bundles.map({ case (bundle, info) =>
    1.15 -                List(HTML.link(bundle, HTML.text(info.platform_description))) }))) :::
    1.16 -          (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link))))))
    1.17 +      HTML.write_document(dir, "index.html",
    1.18 +        List(HTML.title(release_info.name)),
    1.19 +        List(
    1.20 +          HTML.chapter(release_info.name + " (" + release_id + ")"),
    1.21 +          HTML.itemize(
    1.22 +            website_platform_bundles.map({ case (bundle, info) =>
    1.23 +              List(HTML.link(bundle, HTML.text(info.platform_description))) }))) :::
    1.24 +        (if (afp_rev == "") Nil else List(HTML.par(HTML.text("See also ") ::: List(afp_link)))))
    1.25  
    1.26        for ((bundle, _) <- website_platform_bundles)
    1.27          File.copy(release_info.dist_dir + Path.explode(bundle), dir)
     2.1 --- a/src/Pure/Admin/build_status.scala	Sun May 14 21:56:58 2017 +0200
     2.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 14 22:04:52 2017 +0200
     2.3 @@ -203,18 +203,16 @@
     2.4      def clean_name(name: String): String =
     2.5        name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
     2.6  
     2.7 -    HTML.init_dir(target_dir)
     2.8 -    File.write(target_dir + Path.basic("index.html"),
     2.9 -      HTML.output_document(
    2.10 -        List(HTML.title("Isabelle build status")),
    2.11 -        List(HTML.chapter("Isabelle build status"),
    2.12 -          HTML.par(
    2.13 -            List(HTML.description(
    2.14 -              List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
    2.15 -          HTML.par(
    2.16 -            List(HTML.itemize(data.entries.map({ case data_entry =>
    2.17 -              List(HTML.link(clean_name(data_entry.name) + "/index.html",
    2.18 -                HTML.text(data_entry.name))) })))))))
    2.19 +    HTML.write_document(target_dir, "index.html",
    2.20 +      List(HTML.title("Isabelle build status")),
    2.21 +      List(HTML.chapter("Isabelle build status"),
    2.22 +        HTML.par(
    2.23 +          List(HTML.description(
    2.24 +            List(HTML.text("status date:") -> HTML.text(data.date.toString))))),
    2.25 +        HTML.par(
    2.26 +          List(HTML.itemize(data.entries.map({ case data_entry =>
    2.27 +            List(HTML.link(clean_name(data_entry.name) + "/index.html",
    2.28 +              HTML.text(data_entry.name))) }))))))
    2.29  
    2.30      for (data_entry <- data.entries) {
    2.31        val data_name = data_entry.name
    2.32 @@ -308,37 +306,35 @@
    2.33              }
    2.34            }, data_entry.sessions).toMap
    2.35  
    2.36 -      HTML.init_dir(dir)
    2.37 -      File.write(dir + Path.basic("index.html"),
    2.38 -        HTML.output_document(
    2.39 -          List(HTML.title("Isabelle build status for " + data_name)),
    2.40 -          HTML.chapter("Isabelle build status for " + data_name) ::
    2.41 -          HTML.par(
    2.42 -            List(HTML.description(
    2.43 -              List(
    2.44 -                HTML.text("status date:") -> HTML.text(data.date.toString),
    2.45 -                HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) ::
    2.46 -          HTML.par(
    2.47 -            List(HTML.itemize(
    2.48 -              data_entry.sessions.map(session =>
    2.49 -                HTML.link("#session_" + session.name, HTML.text(session.name)) ::
    2.50 -                HTML.text(" (" + session.timing.message_resources + ")"))))) ::
    2.51 -          data_entry.sessions.flatMap(session =>
    2.52 +      HTML.write_document(dir, "index.html",
    2.53 +        List(HTML.title("Isabelle build status for " + data_name)),
    2.54 +        HTML.chapter("Isabelle build status for " + data_name) ::
    2.55 +        HTML.par(
    2.56 +          List(HTML.description(
    2.57              List(
    2.58 -              HTML.section(session.name) + HTML.id("session_" + session.name),
    2.59 -              HTML.par(
    2.60 -                HTML.description(
    2.61 -                  List(
    2.62 -                    HTML.text("timing:") -> HTML.text(session.timing.message_resources),
    2.63 -                    HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) :::
    2.64 -                  proper_string(session.isabelle_version).map(s =>
    2.65 -                    HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
    2.66 -                  proper_string(session.afp_version).map(s =>
    2.67 -                    HTML.text("AFP version:") -> HTML.text(s)).toList) ::
    2.68 -                session_plots.getOrElse(session.name, Nil).map(plot_name =>
    2.69 -                  HTML.image(plot_name) +
    2.70 -                    HTML.width(image_width / 2) +
    2.71 -                    HTML.height(image_height / 2)))))))
    2.72 +              HTML.text("status date:") -> HTML.text(data.date.toString),
    2.73 +              HTML.text("build host:") -> HTML.text(commas(data_entry.hosts)))))) ::
    2.74 +        HTML.par(
    2.75 +          List(HTML.itemize(
    2.76 +            data_entry.sessions.map(session =>
    2.77 +              HTML.link("#session_" + session.name, HTML.text(session.name)) ::
    2.78 +              HTML.text(" (" + session.timing.message_resources + ")"))))) ::
    2.79 +        data_entry.sessions.flatMap(session =>
    2.80 +          List(
    2.81 +            HTML.section(session.name) + HTML.id("session_" + session.name),
    2.82 +            HTML.par(
    2.83 +              HTML.description(
    2.84 +                List(
    2.85 +                  HTML.text("timing:") -> HTML.text(session.timing.message_resources),
    2.86 +                  HTML.text("ML timing:") -> HTML.text(session.ml_timing.message_resources)) :::
    2.87 +                proper_string(session.isabelle_version).map(s =>
    2.88 +                  HTML.text("Isabelle version:") -> HTML.text(s)).toList :::
    2.89 +                proper_string(session.afp_version).map(s =>
    2.90 +                  HTML.text("AFP version:") -> HTML.text(s)).toList) ::
    2.91 +              session_plots.getOrElse(session.name, Nil).map(plot_name =>
    2.92 +                HTML.image(plot_name) +
    2.93 +                  HTML.width(image_width / 2) +
    2.94 +                  HTML.height(image_height / 2))))))
    2.95      }
    2.96    }
    2.97  
     3.1 --- a/src/Pure/Admin/isabelle_devel.scala	Sun May 14 21:56:58 2017 +0200
     3.2 +++ b/src/Pure/Admin/isabelle_devel.scala	Sun May 14 22:04:52 2017 +0200
     3.3 @@ -25,27 +25,25 @@
     3.4    {
     3.5      val header = "Isabelle Development Resources"
     3.6  
     3.7 -    HTML.init_dir(root)
     3.8 -    File.write(root + Path.explode("index.html"),
     3.9 -      HTML.output_document(
    3.10 -        List(HTML.title(header)),
    3.11 -        List(HTML.chapter(header),
    3.12 -          HTML.itemize(
    3.13 -            List(
    3.14 -              HTML.text("Isabelle nightly ") :::
    3.15 -              List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) :::
    3.16 -              HTML.text(" (for all platforms)"),
    3.17 +    HTML.write_document(root, "index.html",
    3.18 +      List(HTML.title(header)),
    3.19 +      List(HTML.chapter(header),
    3.20 +        HTML.itemize(
    3.21 +          List(
    3.22 +            HTML.text("Isabelle nightly ") :::
    3.23 +            List(HTML.link(RELEASE_SNAPSHOT, HTML.text("release snapshot"))) :::
    3.24 +            HTML.text(" (for all platforms)"),
    3.25  
    3.26 -              HTML.text("Isabelle ") :::
    3.27 -              List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) :::
    3.28 -              HTML.text(" information"),
    3.29 +            HTML.text("Isabelle ") :::
    3.30 +            List(HTML.link(BUILD_STATUS + "/index.html", HTML.text("build status"))) :::
    3.31 +            HTML.text(" information"),
    3.32  
    3.33 -              HTML.text("Database with recent ") :::
    3.34 -              List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) :::
    3.35 -              HTML.text(" information (e.g. for ") :::
    3.36 -              List(HTML.link("http://sqlitebrowser.org",
    3.37 -                List(HTML.code(HTML.text("sqlitebrowser"))))) :::
    3.38 -              HTML.text(")"))))))
    3.39 +            HTML.text("Database with recent ") :::
    3.40 +            List(HTML.link(BUILD_LOG_DB, HTML.text("build log"))) :::
    3.41 +            HTML.text(" information (e.g. for ") :::
    3.42 +            List(HTML.link("http://sqlitebrowser.org",
    3.43 +              List(HTML.code(HTML.text("sqlitebrowser"))))) :::
    3.44 +            HTML.text(")")))))
    3.45    }
    3.46  
    3.47  
     4.1 --- a/src/Pure/Thy/html.scala	Sun May 14 21:56:58 2017 +0200
     4.2 +++ b/src/Pure/Thy/html.scala	Sun May 14 22:04:52 2017 +0200
     4.3 @@ -157,12 +157,22 @@
     4.4          output(XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head)),
     4.5          output(XML.elem("body", body))))
     4.6  
     4.7 +
     4.8 +  /* document directory */
     4.9 +
    4.10    def init_dir(dir: Path)
    4.11    {
    4.12      Isabelle_System.mkdirs(dir)
    4.13      File.copy(Path.explode("~~/etc/isabelle.css"), dir)
    4.14    }
    4.15  
    4.16 +  def write_document(dir: Path, name: String, head: XML.Body, body: XML.Body,
    4.17 +    css: String = "isabelle.css")
    4.18 +  {
    4.19 +    init_dir(dir)
    4.20 +    File.write(dir + Path.basic(name), output_document(head, body, css))
    4.21 +  }
    4.22 +
    4.23  
    4.24    /* Isabelle document */
    4.25