make index formally within Isabelle/Scala;

--- a/src/Pure/Admin/isabelle_cronjob.scala	Mon May 08 12:04:58 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Mon May 08 14:08:27 2017 +0200
@@ -39,6 +39,8 @@
   private val build_release =
     Logger_Task("build_release", logger =>
         {
+          Isabelle_Devel.make_index()
+
           val rev = Mercurial.repository(isabelle_repos).id()
           val afp_rev = Mercurial.setup_repository(afp_source, afp_repos).id()
 

--- a/src/Pure/Admin/isabelle_devel.scala	Mon May 08 12:04:58 2017 +0200
+++ b/src/Pure/Admin/isabelle_devel.scala	Mon May 08 14:08:27 2017 +0200
@@ -9,14 +9,43 @@
 
 object Isabelle_Devel
 {
-  val root_dir = Path.explode("~/html-data/devel")
+  val root = Path.explode("~/html-data/devel")
+
+  val RELEASE_SNAPSHOT = "release_snapshot"
+  val BUILD_LOG_DB = "build_log.db"
+  val BUILD_STATUS = "build_status"
+
+  val standard_log_dirs =
+    List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
+
+
+  /* index */
+
+  def make_index()
+  {
+    val header = "Isabelle Development Resources"
 
-  val release_snapshot_dir = root_dir + Path.explode("release_snapshot")
-  val build_log_db = root_dir + Path.explode("build_log.db")
-  val build_status_dir = root_dir + Path.explode("build_status")
+    Isabelle_System.mkdirs(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)"),
 
-  val log_dirs =
-    List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
+              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"))))))))))
+  }
 
 
   /* release snapshot */
@@ -29,6 +58,8 @@
   {
     Isabelle_System.with_tmp_dir("isadist")(base_dir =>
       {
+        val release_snapshot_dir = root + Path.explode(RELEASE_SNAPSHOT)
+
         val new_snapshot = release_snapshot_dir.ext("new")
         val old_snapshot = release_snapshot_dir.ext("old")
 
@@ -47,13 +78,13 @@
 
   /* maintain build_log database */
 
-  def build_log_database(options: Options)
+  def build_log_database(options: Options, log_dirs: List[Path] = standard_log_dirs)
   {
     val store = Build_Log.store(options)
     using(store.open_database())(db =>
     {
       store.update_database(db, log_dirs, ml_statistics = true)
-      store.snapshot_database(db, build_log_db)
+      store.snapshot_database(db, root + Path.explode(BUILD_LOG_DB))
     })
   }
 
@@ -63,6 +94,6 @@
   def build_status(options: Options)
   {
     val data = Build_Status.read_data(options)
-    Build_Status.present_data(data, target_dir = build_status_dir)
+    Build_Status.present_data(data, target_dir = root + Path.explode(BUILD_STATUS))
   }
 }

--- a/src/Pure/Thy/html.scala	Mon May 08 12:04:58 2017 +0200
+++ b/src/Pure/Thy/html.scala	Mon May 08 14:08:27 2017 +0200
@@ -103,6 +103,7 @@
   val par = new Operator("p")
   val emph = new Operator("em")
   val bold = new Operator("b")
+  val code = new Operator("code")
 
   val title = new Heading("title")
   val chapter = new Heading("h1")