# HG changeset patch
# User wenzelm
# Date 1574682112 -3600
# Node ID a21a29de5f57ed758c474459b935ea062f06ef03
# Parent  b5822f4c3fdecc0c6d34db287d29dbd812ce019e
tuned;

diff -r b5822f4c3fde -r a21a29de5f57 src/Pure/General/output.scala
--- a/src/Pure/General/output.scala	Mon Nov 25 12:19:14 2019 +0100
+++ b/src/Pure/General/output.scala	Mon Nov 25 12:41:52 2019 +0100
@@ -16,10 +16,10 @@
   def writeln_text(msg: String): String = clean_yxml(msg)
 
   def warning_text(msg: String): String =
-    cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
+    Library.prefix_lines("### ", clean_yxml(msg))
 
   def error_message_text(msg: String): String =
-    cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
+    Library.prefix_lines("*** ", clean_yxml(msg))
 
   def writeln(msg: String, stdout: Boolean = false, include_empty: Boolean = false)
   {
diff -r b5822f4c3fde -r a21a29de5f57 src/Pure/Thy/latex.scala
--- a/src/Pure/Thy/latex.scala	Mon Nov 25 12:19:14 2019 +0100
+++ b/src/Pure/Thy/latex.scala	Mon Nov 25 12:41:52 2019 +0100
@@ -21,7 +21,7 @@
     val root_log_path = dir + Path.explode(root_name).ext("log")
     if (root_log_path.is_file) {
       for { (msg, pos) <- filter_errors(dir, File.read(root_log_path)) }
-      yield "Latex error" + Position.here(pos) + ":\n" + cat_lines(split_lines(msg).map("  " + _))
+      yield "Latex error" + Position.here(pos) + ":\n" + Library.prefix_lines("  ", msg)
     }
     else Nil
   }
diff -r b5822f4c3fde -r a21a29de5f57 src/Pure/library.scala
--- a/src/Pure/library.scala	Mon Nov 25 12:19:14 2019 +0100
+++ b/src/Pure/library.scala	Mon Nov 25 12:41:52 2019 +0100
@@ -103,8 +103,7 @@
   def split_lines(str: String): List[String] = space_explode('\n', str)
 
   def prefix_lines(prfx: String, str: String): String =
-    if (str == "") str
-    else cat_lines(split_lines(str).map(s => prfx + s))
+    if (str == "") str else cat_lines(split_lines(str).map(prfx + _))
 
   def first_line(source: CharSequence): String =
   {