more systematic HTML.init_dir with css;
authorwenzelm
Sun May 14 21:54:35 2017 +0200 (2017-05-14)
changeset 658363b4877fbd9cb
parent 65835 5ec497351636
child 65837 9ee6a8d4499b
more systematic HTML.init_dir with css;
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:34:36 2017 +0200
     1.2 +++ b/src/Pure/Admin/build_release.scala	Sun May 14 21:54:35 2017 +0200
     1.3 @@ -123,12 +123,11 @@
     1.4              info.all_bundles.find(name => (release_info.dist_dir + Path.explode(name)).is_file)
     1.5          } yield (bundle, info)
     1.6  
     1.7 -      Isabelle_System.mkdirs(dir)
     1.8 -
     1.9        val afp_link =
    1.10          HTML.link("https://bitbucket.org/isa-afp/afp-devel/commits/" + afp_rev,
    1.11            HTML.text("AFP/" + afp_rev))
    1.12  
    1.13 +      HTML.init_dir(dir)
    1.14        File.write(dir + Path.explode("index.html"),
    1.15          HTML.output_document(
    1.16            List(HTML.title(release_info.name)),
     2.1 --- a/src/Pure/Admin/build_status.scala	Sun May 14 21:34:36 2017 +0200
     2.2 +++ b/src/Pure/Admin/build_status.scala	Sun May 14 21:54:35 2017 +0200
     2.3 @@ -203,7 +203,7 @@
     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 -    Isabelle_System.mkdirs(target_dir)
     2.8 +    HTML.init_dir(target_dir)
     2.9      File.write(target_dir + Path.basic("index.html"),
    2.10        HTML.output_document(
    2.11          List(HTML.title("Isabelle build status")),
    2.12 @@ -308,6 +308,7 @@
    2.13              }
    2.14            }, data_entry.sessions).toMap
    2.15  
    2.16 +      HTML.init_dir(dir)
    2.17        File.write(dir + Path.basic("index.html"),
    2.18          HTML.output_document(
    2.19            List(HTML.title("Isabelle build status for " + data_name)),
     3.1 --- a/src/Pure/Admin/isabelle_devel.scala	Sun May 14 21:34:36 2017 +0200
     3.2 +++ b/src/Pure/Admin/isabelle_devel.scala	Sun May 14 21:54:35 2017 +0200
     3.3 @@ -25,7 +25,7 @@
     3.4    {
     3.5      val header = "Isabelle Development Resources"
     3.6  
     3.7 -    Isabelle_System.mkdirs(root)
     3.8 +    HTML.init_dir(root)
     3.9      File.write(root + Path.explode("index.html"),
    3.10        HTML.output_document(
    3.11          List(HTML.title(header)),
     4.1 --- a/src/Pure/Thy/html.scala	Sun May 14 21:34:36 2017 +0200
     4.2 +++ b/src/Pure/Thy/html.scala	Sun May 14 21:54:35 2017 +0200
     4.3 @@ -148,12 +148,21 @@
     4.4      XML.Elem(Markup("meta",
     4.5        List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
     4.6  
     4.7 -  def output_document(head: XML.Body, body: XML.Body): String =
     4.8 +  def head_css(css: String): XML.Elem =
     4.9 +    XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil)
    4.10 +
    4.11 +  def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css"): String =
    4.12      cat_lines(
    4.13        List(header,
    4.14 -        output(XML.elem("head", head_meta :: head)),
    4.15 +        output(XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head)),
    4.16          output(XML.elem("body", body))))
    4.17  
    4.18 +  def init_dir(dir: Path)
    4.19 +  {
    4.20 +    Isabelle_System.mkdirs(dir)
    4.21 +    File.copy(Path.explode("~~/etc/isabelle.css"), dir)
    4.22 +  }
    4.23 +
    4.24  
    4.25    /* Isabelle document */
    4.26