--- 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)))
--- 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 =
--- 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 =
--- 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 =