# HG changeset patch # User wenzelm # Date 1476302010 -7200 # Node ID 85ff21510ba9e788451154e24d0e152e6b56b4bc # Parent e7863057df412a616e251ade9cddcf6283ebfc45 tuned signature; diff -r e7863057df41 -r 85ff21510ba9 src/Pure/Admin/build_history.scala --- a/src/Pure/Admin/build_history.scala Wed Oct 12 21:50:16 2016 +0200 +++ b/src/Pure/Admin/build_history.scala Wed Oct 12 21:53:30 2016 +0200 @@ -78,7 +78,7 @@ "init_components " + File.bash_path(components_base_path) + " \"$ISABELLE_HOME/Admin/components/" + catalog + "\"") } - File.append(etc_settings, "\n" + Library.terminate_lines(component_settings)) + File.append(etc_settings, "\n" + terminate_lines(component_settings)) } @@ -147,7 +147,7 @@ List(ml_settings, thread_settings) ::: (if (more_settings.isEmpty) Nil else List(more_settings)) - File.append(etc_settings, "\n" + cat_lines(settings.map(Library.terminate_lines(_)))) + File.append(etc_settings, "\n" + cat_lines(settings.map(terminate_lines(_)))) ml_platform } @@ -287,7 +287,7 @@ Isabelle_System.mkdirs(log_path.dir) File.write_gzip(log_path, - Library.terminate_lines( + terminate_lines( Build_Log.Log_File.print_props(META_INFO_MARKER, meta_info) :: res.out_lines ::: ml_statistics.map(Build_Log.Log_File.print_props(Build_Log.ML_STATISTICS_MARKER, _)) ::: heap_sizes)) diff -r e7863057df41 -r 85ff21510ba9 src/Pure/Admin/isabelle_cronjob.scala --- a/src/Pure/Admin/isabelle_cronjob.scala Wed Oct 12 21:50:16 2016 +0200 +++ b/src/Pure/Admin/isabelle_cronjob.scala Wed Oct 12 21:53:30 2016 +0200 @@ -114,7 +114,7 @@ val log_path = log_dir + Build_Log.log_path("isabelle_identify", logger.start_date) Isabelle_System.mkdirs(log_path.dir) File.write(log_path, - Library.terminate_lines( + terminate_lines( List("isabelle_identify: " + Build_Log.print_date(logger.start_date), "", "Isabelle version: " + isabelle_id, diff -r e7863057df41 -r 85ff21510ba9 src/Pure/ROOT.scala --- a/src/Pure/ROOT.scala Wed Oct 12 21:50:16 2016 +0200 +++ b/src/Pure/ROOT.scala Wed Oct 12 21:53:30 2016 +0200 @@ -15,6 +15,7 @@ val space_explode = Library.space_explode _ val split_lines = Library.split_lines _ val cat_lines = Library.cat_lines _ + val terminate_lines = Library.terminate_lines _ val quote = Library.quote _ val commas = Library.commas _ val commas_quote = Library.commas_quote _ diff -r e7863057df41 -r 85ff21510ba9 src/Pure/Tools/build.scala --- a/src/Pure/Tools/build.scala Wed Oct 12 21:50:16 2016 +0200 +++ b/src/Pure/Tools/build.scala Wed Oct 12 21:53:30 2016 +0200 @@ -562,7 +562,7 @@ yield Sessions.write_heap_digest(path) File.write_gzip(store.output_dir + Sessions.log_gz(name), - Library.terminate_lines( + terminate_lines( session_sources_stamp(name) :: input_heaps.map(INPUT_HEAP + _) ::: heap_stamp.toList.map(OUTPUT_HEAP + _) ::: @@ -575,7 +575,7 @@ (store.output_dir + Sessions.log_gz(name)).file.delete File.write(store.output_dir + Sessions.log(name), - Library.terminate_lines(process_result.out_lines)) + terminate_lines(process_result.out_lines)) progress.echo(name + " FAILED") if (!process_result.interrupted) progress.echo(process_result_tail.out)