--- 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))
--- 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,
--- 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 _
--- 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)