# HG changeset patch
# User wenzelm
# Date 1494791675 -7200
# Node ID 3b4877fbd9cbc61a0fec3654d39df95567da712d
# Parent  5ec49735163689c34159ec40e5be11741b30b9e5
more systematic HTML.init_dir with css;

diff -r 5ec497351636 -r 3b4877fbd9cb src/Pure/Admin/build_release.scala
--- a/src/Pure/Admin/build_release.scala	Sun May 14 21:34:36 2017 +0200
+++ b/src/Pure/Admin/build_release.scala	Sun May 14 21:54:35 2017 +0200
@@ -123,12 +123,11 @@
             info.all_bundles.find(name => (release_info.dist_dir + Path.explode(name)).is_file)
         } yield (bundle, info)
 
-      Isabelle_System.mkdirs(dir)
-
       val afp_link =
         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)),
diff -r 5ec497351636 -r 3b4877fbd9cb src/Pure/Admin/build_status.scala
--- a/src/Pure/Admin/build_status.scala	Sun May 14 21:34:36 2017 +0200
+++ b/src/Pure/Admin/build_status.scala	Sun May 14 21:54:35 2017 +0200
@@ -203,7 +203,7 @@
     def clean_name(name: String): String =
       name.flatMap(c => if (c == ' ' || c == '/') "_" else if (c == ',') "" else c.toString)
 
-    Isabelle_System.mkdirs(target_dir)
+    HTML.init_dir(target_dir)
     File.write(target_dir + Path.basic("index.html"),
       HTML.output_document(
         List(HTML.title("Isabelle build status")),
@@ -308,6 +308,7 @@
             }
           }, 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)),
diff -r 5ec497351636 -r 3b4877fbd9cb src/Pure/Admin/isabelle_devel.scala
--- a/src/Pure/Admin/isabelle_devel.scala	Sun May 14 21:34:36 2017 +0200
+++ b/src/Pure/Admin/isabelle_devel.scala	Sun May 14 21:54:35 2017 +0200
@@ -25,7 +25,7 @@
   {
     val header = "Isabelle Development Resources"
 
-    Isabelle_System.mkdirs(root)
+    HTML.init_dir(root)
     File.write(root + Path.explode("index.html"),
       HTML.output_document(
         List(HTML.title(header)),
diff -r 5ec497351636 -r 3b4877fbd9cb src/Pure/Thy/html.scala
--- a/src/Pure/Thy/html.scala	Sun May 14 21:34:36 2017 +0200
+++ b/src/Pure/Thy/html.scala	Sun May 14 21:54:35 2017 +0200
@@ -148,12 +148,21 @@
     XML.Elem(Markup("meta",
       List("http-equiv" -> "Content-Type", "content" -> "text/html; charset=utf-8")), Nil)
 
-  def output_document(head: XML.Body, body: XML.Body): String =
+  def head_css(css: String): XML.Elem =
+    XML.Elem(Markup("link", List("rel" -> "stylesheet", "type" -> "text/css", "href" -> css)), Nil)
+
+  def output_document(head: XML.Body, body: XML.Body, css: String = "isabelle.css"): String =
     cat_lines(
       List(header,
-        output(XML.elem("head", head_meta :: head)),
+        output(XML.elem("head", head_meta :: (if (css == "") Nil else List(head_css(css))) ::: head)),
         output(XML.elem("body", body))))
 
+  def init_dir(dir: Path)
+  {
+    Isabelle_System.mkdirs(dir)
+    File.copy(Path.explode("~~/etc/isabelle.css"), dir)
+  }
+
 
   /* Isabelle document */