some timing and logging, similar to old isatest.log;

--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 21:44:20 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 21:48:56 2016 +0200
@@ -9,6 +9,64 @@
 
 object Isabelle_Cronjob
 {
+  /** file-system state: owned by main cronjob **/
+
+  val main_dir = Path.explode("~/cronjob")
+  val run_dir = main_dir + Path.explode("run")
+  val log_dir = main_dir + Path.explode("log")
+
+  val main_state_file = run_dir + Path.explode("main.state")
+  val main_log = log_dir + Path.explode("main.log")
+
+
+
+  /** cronjob **/
+
+  def cronjob(progress: Progress)
+  {
+    /* log */
+
+    val hostname = Isabelle_System.hostname()
+
+    def log(date: Date, msg: String)
+    {
+      val text = "[" + Build_Log.Log_File.Date_Format(date) + " " + hostname + "]: " + msg
+      File.append(main_log, text + "\n")
+      progress.echo(text)
+    }
+
+
+    /* start */
+
+    val start_date = Date.now()
+
+    val still_running =
+      try { Some(File.read(main_state_file)) }
+      catch { case ERROR(_) => None }
+
+    still_running match {
+      case Some(running) =>
+        error("Isabelle cronjob appears to be still running: " + running)
+      case None =>
+        File.write(main_state_file, start_date + " " + hostname)
+        log(start_date, "start cronjob")
+    }
+
+
+    /* end */
+
+    val end_date = Date.now()
+    val elapsed_time = end_date.time - start_date.time
+
+    log(end_date, "end cronjob, elapsed time " + elapsed_time.message_hms)
+
+    main_state_file.file.delete
+  }
+
+
+
+  /** command line entry point **/
+
   def main(args: Array[String])
   {
     Command_Line.tool0 {
@@ -28,16 +86,10 @@
       val more_args = getopts(args)
       if (more_args.nonEmpty) getopts.usage()
 
-      if (verbose) Output.writeln("This is the Isabelle cronjob")
+      val progress = if (verbose) new Console_Progress() else Ignore_Progress
 
-      val rc =
-        if (force) {
-          Thread.sleep(Time.seconds(30).ms)
-          0
-        }
-        else { Output.warning("Need to apply force to do anything"); 1 }
-
-      if (rc != 0) sys.exit(rc)
+      if (force) cronjob(progress)
+      else error("Need to apply force to do anything")
     }
   }
 }