tuned signature;
authorwenzelm
Wed, 12 Oct 2016 21:53:30 +0200
changeset 64173 85ff21510ba9
parent 64172 e7863057df41
child 64174 54479f7b6685
tuned signature;
src/Pure/Admin/build_history.scala
src/Pure/Admin/isabelle_cronjob.scala
src/Pure/ROOT.scala
src/Pure/Tools/build.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))
--- 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)