# HG changeset patch
# User wenzelm
# Date 1494774306 -7200
# Node ID 02dd430d80c56480cd6b1f2ef12ca93e28167e62
# Parent  3bba3856b56c7563b546d601bdb66c2bd07b80dc
tuned signature;

diff -r 3bba3856b56c -r 02dd430d80c5 src/Pure/General/exn.scala
--- a/src/Pure/General/exn.scala	Sun May 14 17:01:05 2017 +0200
+++ b/src/Pure/General/exn.scala	Sun May 14 17:05:06 2017 +0200
@@ -20,7 +20,7 @@
       }
     override def hashCode: Int = message.hashCode
 
-    override def toString: String = "\n" + Output.error_text(message)
+    override def toString: String = "\n" + Output.error_message_text(message)
   }
 
   object ERROR
diff -r 3bba3856b56c -r 02dd430d80c5 src/Pure/General/http.scala
--- a/src/Pure/General/http.scala	Sun May 14 17:01:05 2017 +0200
+++ b/src/Pure/General/http.scala	Sun May 14 17:05:06 2017 +0200
@@ -77,7 +77,7 @@
             case Exn.Res(None) =>
               http.write_response(404, Response.empty)
             case Exn.Exn(ERROR(msg)) =>
-              http.write_response(500, Response.text(Output.error_text(msg)))
+              http.write_response(500, Response.text(Output.error_message_text(msg)))
             case Exn.Exn(exn) => throw exn
           }
         else http.write_response(400, Response.empty)
diff -r 3bba3856b56c -r 02dd430d80c5 src/Pure/General/output.scala
--- a/src/Pure/General/output.scala	Sun May 14 17:01:05 2017 +0200
+++ b/src/Pure/General/output.scala	Sun May 14 17:05:06 2017 +0200
@@ -14,8 +14,12 @@
     catch { case ERROR(_) => msg }
 
   def writeln_text(msg: String): String = clean_yxml(msg)
-  def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
-  def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
+
+  def warning_text(msg: String): String =
+    cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
+
+  def error_message_text(msg: String): String =
+    cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
 
   def writeln(msg: String, stdout: Boolean = false)
   {
@@ -36,8 +40,8 @@
   def error_message(msg: String, stdout: Boolean = false)
   {
     if (msg != "") {
-      if (stdout) Console.println(error_text(msg))
-      else Console.err.println(error_text(msg))
+      if (stdout) Console.println(error_message_text(msg))
+      else Console.err.println(error_message_text(msg))
     }
   }
 }
diff -r 3bba3856b56c -r 02dd430d80c5 src/Pure/System/progress.scala
--- a/src/Pure/System/progress.scala	Sun May 14 17:01:05 2017 +0200
+++ b/src/Pure/System/progress.scala	Sun May 14 17:05:06 2017 +0200
@@ -17,7 +17,7 @@
   def theory(session: String, theory: String) {}
 
   def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
-  def echo_error(msg: String) { echo(Output.error_text(msg)) }
+  def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
 
   def stopped: Boolean = false
   override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
diff -r 3bba3856b56c -r 02dd430d80c5 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun May 14 17:01:05 2017 +0200
+++ b/src/Pure/Tools/build.scala	Sun May 14 17:05:06 2017 +0200
@@ -245,7 +245,7 @@
             case msg =>
               result.copy(
                 rc = result.rc max 1,
-                out_lines = result.out_lines ::: split_lines(Output.error_text(msg)))
+                out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg)))
           }
         }
         else {
@@ -309,8 +309,8 @@
       timeout_request.foreach(_.cancel)
 
       if (result.interrupted) {
-        if (was_timeout) result.error(Output.error_text("Timeout")).was_timeout
-        else result.error(Output.error_text("Interrupt"))
+        if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
+        else result.error(Output.error_message_text("Interrupt"))
       }
       else result
     }
diff -r 3bba3856b56c -r 02dd430d80c5 src/Tools/jEdit/src/session_build.scala
--- a/src/Tools/jEdit/src/session_build.scala	Sun May 14 17:01:05 2017 +0200
+++ b/src/Tools/jEdit/src/session_build.scala	Sun May 14 17:05:06 2017 +0200
@@ -173,7 +173,7 @@
         try { ("", JEdit_Sessions.session_build(options, progress = progress)) }
         catch {
           case exn: Throwable =>
-            (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
+            (Output.error_message_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
         }
 
       progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))