# HG changeset patch
# User wenzelm
# Date 1494356771 -7200
# Node ID 96b4799a2e04f0f6cd22a55ea6e8ef682319875e
# Parent  c58752102b3400d185494d6086468bef3c40dea6
more robust update of generated directory;
tuned;

diff -r c58752102b34 -r 96b4799a2e04 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue May 09 20:36:34 2017 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue May 09 21:06:11 2017 +0200
@@ -360,9 +360,7 @@
             Logger_Task("build_log_database",
               logger => Isabelle_Devel.build_log_database(logger.options)),
             Logger_Task("build_status",
-              logger =>
-                Build_Status.build_status(logger.options,
-                  target_dir = Isabelle_Devel.build_status_dir)))))))
+              logger => Isabelle_Devel.build_status(logger.options)))))))
 
     log_service.shutdown()
 
diff -r c58752102b34 -r 96b4799a2e04 src/Pure/Admin/isabelle_devel.scala
--- a/src/Pure/Admin/isabelle_devel.scala	Tue May 09 20:36:34 2017 +0200
+++ b/src/Pure/Admin/isabelle_devel.scala	Tue May 09 21:06:11 2017 +0200
@@ -18,8 +18,6 @@
   val standard_log_dirs =
     List(Path.explode("~/log"), Path.explode("~/afp/log"), Path.explode("~/cronjob/log"))
 
-  val build_status_dir = root + Path.explode(BUILD_STATUS)
-
 
   /* index */
 
@@ -60,20 +58,10 @@
   {
     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")
-
-        Isabelle_System.rm_tree(new_snapshot)
-        Isabelle_System.rm_tree(old_snapshot)
-
-        Build_Release.build_release(base_dir, rev = rev, afp_rev = afp_rev,
-          parallel_jobs = parallel_jobs, remote_mac = remote_mac, website = Some(new_snapshot))
-
-        if (release_snapshot_dir.is_dir) File.move(release_snapshot_dir, old_snapshot)
-        File.move(new_snapshot, release_snapshot_dir)
-        Isabelle_System.rm_tree(old_snapshot)
+        Isabelle_System.update_directory(root + Path.explode(RELEASE_SNAPSHOT),
+          website_dir =>
+            Build_Release.build_release(base_dir, rev = rev, afp_rev = afp_rev,
+              parallel_jobs = parallel_jobs, remote_mac = remote_mac, website = Some(website_dir)))
       })
   }
 
@@ -89,4 +77,13 @@
       store.snapshot_database(db, root + Path.explode(BUILD_LOG_DB))
     })
   }
+
+
+  /* present build status */
+
+  def build_status(options: Options)
+  {
+    Isabelle_System.update_directory(root + Path.explode(BUILD_STATUS),
+      dir => Build_Status.build_status(options, target_dir = dir))
+  }
 }
diff -r c58752102b34 -r 96b4799a2e04 src/Pure/System/isabelle_system.scala
--- a/src/Pure/System/isabelle_system.scala	Tue May 09 20:36:34 2017 +0200
+++ b/src/Pure/System/isabelle_system.scala	Tue May 09 21:06:11 2017 +0200
@@ -237,6 +237,24 @@
   }
 
 
+  /* quasi-atomic update of directory */
+
+  def update_directory(dir: Path, f: Path => Unit)
+  {
+    val new_dir = dir.ext("new")
+    val old_dir = dir.ext("old")
+
+    rm_tree(new_dir)
+    rm_tree(old_dir)
+
+    f(new_dir)
+
+    if (dir.is_dir) File.move(dir, old_dir)
+    File.move(new_dir, dir)
+    rm_tree(old_dir)
+  }
+
+
 
   /** external processes **/