tuned signature;
authorwenzelm
Tue Oct 11 22:24:14 2016 +0200 (2016-10-11)
changeset 64155646c4d6a6a02
parent 64154 e5cf40a54b1e
child 64156 01716e3c3e68
tuned signature;
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/Tools/build.scala
src/Pure/Tools/build_history.scala
src/Pure/Tools/build_log.scala
     1.1 --- a/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 22:14:26 2016 +0200
     1.2 +++ b/src/Pure/Admin/isabelle_cronjob.scala	Tue Oct 11 22:24:14 2016 +0200
     1.3 @@ -42,7 +42,7 @@
     1.4  
     1.5      def log(date: Date, msg: String)
     1.6      {
     1.7 -      val text = "[" + Build_Log.Log_File.Date_Format(date) + " " + hostname + "]: " + msg
     1.8 +      val text = "[" + Build_Log.print_date(date) + " " + hostname + "]: " + msg
     1.9        File.append(main_log, text + "\n")
    1.10        progress.echo(text)
    1.11      }
    1.12 @@ -77,7 +77,7 @@
    1.13        Isabelle_System.mkdirs(log_path.dir)
    1.14        File.write(log_path,
    1.15          Library.terminate_lines(
    1.16 -          List("isabelle_identify: " + Build_Log.Log_File.Date_Format(pull_date),
    1.17 +          List("isabelle_identify: " + Build_Log.print_date(pull_date),
    1.18              "",
    1.19              "Isabelle version: " + isabelle_id,
    1.20              "AFP version: " + afp_id)))
     2.1 --- a/src/Pure/Tools/build.scala	Tue Oct 11 22:14:26 2016 +0200
     2.2 +++ b/src/Pure/Tools/build.scala	Tue Oct 11 22:24:14 2016 +0200
     2.3 @@ -756,7 +756,7 @@
     2.4  
     2.5      if (verbose) {
     2.6        progress.echo(
     2.7 -        "Started at " + Build_Log.Log_File.Date_Format(start_date) +
     2.8 +        "Started at " + Build_Log.print_date(start_date) +
     2.9            " (" + Isabelle_System.getenv("ML_IDENTIFIER") + " on " + Isabelle_System.hostname() +")")
    2.10        progress.echo(Build_Log.Settings.show() + "\n")
    2.11      }
    2.12 @@ -785,7 +785,7 @@
    2.13      val elapsed_time = end_date.time - start_date.time
    2.14  
    2.15      if (verbose) {
    2.16 -      progress.echo("\nFinished at " + Build_Log.Log_File.Date_Format(end_date))
    2.17 +      progress.echo("\nFinished at " + Build_Log.print_date(end_date))
    2.18      }
    2.19  
    2.20      val total_timing =
     3.1 --- a/src/Pure/Tools/build_history.scala	Tue Oct 11 22:14:26 2016 +0200
     3.2 +++ b/src/Pure/Tools/build_history.scala	Tue Oct 11 22:24:14 2016 +0200
     3.3 @@ -261,8 +261,8 @@
     3.4        val meta_info =
     3.5          List(Build_Log.Field.build_engine -> BUILD_HISTORY,
     3.6            Build_Log.Field.build_host -> build_host,
     3.7 -          Build_Log.Field.build_start -> Build_Log.Log_File.Date_Format(build_start),
     3.8 -          Build_Log.Field.build_end -> Build_Log.Log_File.Date_Format(build_end),
     3.9 +          Build_Log.Field.build_start -> Build_Log.print_date(build_start),
    3.10 +          Build_Log.Field.build_end -> Build_Log.print_date(build_end),
    3.11            Build_Log.Field.isabelle_version -> isabelle_version)
    3.12  
    3.13        val ml_statistics =
     4.1 --- a/src/Pure/Tools/build_log.scala	Tue Oct 11 22:14:26 2016 +0200
     4.2 +++ b/src/Pure/Tools/build_log.scala	Tue Oct 11 22:24:14 2016 +0200
     4.3 @@ -79,6 +79,8 @@
     4.4  
     4.5    /** log file **/
     4.6  
     4.7 +  def print_date(date: Date): String = Log_File.Date_Format(date)
     4.8 +
     4.9    object Log_File
    4.10    {
    4.11      def apply(name: String, lines: List[String]): Log_File =