# HG changeset patch
# User wenzelm
# Date 1476217454 -7200
# Node ID 646c4d6a6a02435a052b26e3ee86bb2d51acf9ac
# Parent  e5cf40a54b1ece527bdc75665fad075249461e02
tuned signature;

diff -r e5cf40a54b1e -r 646c4d6a6a02 src/Pure/Admin/isabelle_cronjob.scala
--- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 22:14:26 2016 +0200
+++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 22:24:14 2016 +0200
@@ -42,7 +42,7 @@
 
     def log(date: Date, msg: String)
     {
-      val text = "[" + Build_Log.Log_File.Date_Format(date) + " " + hostname + "]: " + msg
+      val text = "[" + Build_Log.print_date(date) + " " + hostname + "]: " + msg
       File.append(main_log, text + "\n")
       progress.echo(text)
     }
@@ -77,7 +77,7 @@
       Isabelle_System.mkdirs(log_path.dir)
       File.write(log_path,
         Library.terminate_lines(
-          List("isabelle_identify: " + Build_Log.Log_File.Date_Format(pull_date),
+          List("isabelle_identify: " + Build_Log.print_date(pull_date),
             "",
             "Isabelle version: " + isabelle_id,
             "AFP version: " + afp_id)))
diff -r e5cf40a54b1e -r 646c4d6a6a02 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Tue Oct 11 22:14:26 2016 +0200
+++ b/src/Pure/Tools/build.scala	Tue Oct 11 22:24:14 2016 +0200
@@ -756,7 +756,7 @@
 
     if (verbose) {
       progress.echo(
-        "Started at " + Build_Log.Log_File.Date_Format(start_date) +
+        "Started at " + Build_Log.print_date(start_date) +
           " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
       progress.echo(Build_Log.Settings.show() + "\n")
     }
@@ -785,7 +785,7 @@
     val elapsed_time = end_date.time - start_date.time
 
     if (verbose) {
-      progress.echo("\nFinished at " + Build_Log.Log_File.Date_Format(end_date))
+      progress.echo("\nFinished at " + Build_Log.print_date(end_date))
     }
 
     val total_timing =
diff -r e5cf40a54b1e -r 646c4d6a6a02 src/Pure/Tools/build_history.scala
--- a/src/Pure/Tools/build_history.scala	Tue Oct 11 22:14:26 2016 +0200
+++ b/src/Pure/Tools/build_history.scala	Tue Oct 11 22:24:14 2016 +0200
@@ -261,8 +261,8 @@
       val meta_info =
         List(Build_Log.Field.build_engine -> BUILD_HISTORY,
           Build_Log.Field.build_host -> build_host,
-          Build_Log.Field.build_start -> Build_Log.Log_File.Date_Format(build_start),
-          Build_Log.Field.build_end -> Build_Log.Log_File.Date_Format(build_end),
+          Build_Log.Field.build_start -> Build_Log.print_date(build_start),
+          Build_Log.Field.build_end -> Build_Log.print_date(build_end),
           Build_Log.Field.isabelle_version -> isabelle_version)
 
       val ml_statistics =
diff -r e5cf40a54b1e -r 646c4d6a6a02 src/Pure/Tools/build_log.scala
--- a/src/Pure/Tools/build_log.scala	Tue Oct 11 22:14:26 2016 +0200
+++ b/src/Pure/Tools/build_log.scala	Tue Oct 11 22:24:14 2016 +0200
@@ -79,6 +79,8 @@
 
   /** log file **/
 
+  def print_date(date: Date): String = Log_File.Date_Format(date)
+
   object Log_File
   {
     def apply(name: String, lines: List[String]): Log_File =