tuned signature;
authorwenzelm
Sun May 14 17:05:06 2017 +0200 (2017-05-14)
changeset 6582802dd430d80c5
parent 65827 3bba3856b56c
child 65829 07e86b942a84
tuned signature;
src/Pure/General/exn.scala
src/Pure/General/http.scala
src/Pure/General/output.scala
src/Pure/System/progress.scala
src/Pure/Tools/build.scala
src/Tools/jEdit/src/session_build.scala
     1.1 --- a/src/Pure/General/exn.scala	Sun May 14 17:01:05 2017 +0200
     1.2 +++ b/src/Pure/General/exn.scala	Sun May 14 17:05:06 2017 +0200
     1.3 @@ -20,7 +20,7 @@
     1.4        }
     1.5      override def hashCode: Int = message.hashCode
     1.6  
     1.7 -    override def toString: String = "\n" + Output.error_text(message)
     1.8 +    override def toString: String = "\n" + Output.error_message_text(message)
     1.9    }
    1.10  
    1.11    object ERROR
     2.1 --- a/src/Pure/General/http.scala	Sun May 14 17:01:05 2017 +0200
     2.2 +++ b/src/Pure/General/http.scala	Sun May 14 17:05:06 2017 +0200
     2.3 @@ -77,7 +77,7 @@
     2.4              case Exn.Res(None) =>
     2.5                http.write_response(404, Response.empty)
     2.6              case Exn.Exn(ERROR(msg)) =>
     2.7 -              http.write_response(500, Response.text(Output.error_text(msg)))
     2.8 +              http.write_response(500, Response.text(Output.error_message_text(msg)))
     2.9              case Exn.Exn(exn) => throw exn
    2.10            }
    2.11          else http.write_response(400, Response.empty)
     3.1 --- a/src/Pure/General/output.scala	Sun May 14 17:01:05 2017 +0200
     3.2 +++ b/src/Pure/General/output.scala	Sun May 14 17:05:06 2017 +0200
     3.3 @@ -14,8 +14,12 @@
     3.4      catch { case ERROR(_) => msg }
     3.5  
     3.6    def writeln_text(msg: String): String = clean_yxml(msg)
     3.7 -  def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
     3.8 -  def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
     3.9 +
    3.10 +  def warning_text(msg: String): String =
    3.11 +    cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
    3.12 +
    3.13 +  def error_message_text(msg: String): String =
    3.14 +    cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
    3.15  
    3.16    def writeln(msg: String, stdout: Boolean = false)
    3.17    {
    3.18 @@ -36,8 +40,8 @@
    3.19    def error_message(msg: String, stdout: Boolean = false)
    3.20    {
    3.21      if (msg != "") {
    3.22 -      if (stdout) Console.println(error_text(msg))
    3.23 -      else Console.err.println(error_text(msg))
    3.24 +      if (stdout) Console.println(error_message_text(msg))
    3.25 +      else Console.err.println(error_message_text(msg))
    3.26      }
    3.27    }
    3.28  }
     4.1 --- a/src/Pure/System/progress.scala	Sun May 14 17:01:05 2017 +0200
     4.2 +++ b/src/Pure/System/progress.scala	Sun May 14 17:05:06 2017 +0200
     4.3 @@ -17,7 +17,7 @@
     4.4    def theory(session: String, theory: String) {}
     4.5  
     4.6    def echo_warning(msg: String) { echo(Output.warning_text(msg)) }
     4.7 -  def echo_error(msg: String) { echo(Output.error_text(msg)) }
     4.8 +  def echo_error_message(msg: String) { echo(Output.error_message_text(msg)) }
     4.9  
    4.10    def stopped: Boolean = false
    4.11    override def toString: String = if (stopped) "Progress(stopped)" else "Progress"
     5.1 --- a/src/Pure/Tools/build.scala	Sun May 14 17:01:05 2017 +0200
     5.2 +++ b/src/Pure/Tools/build.scala	Sun May 14 17:05:06 2017 +0200
     5.3 @@ -245,7 +245,7 @@
     5.4              case msg =>
     5.5                result.copy(
     5.6                  rc = result.rc max 1,
     5.7 -                out_lines = result.out_lines ::: split_lines(Output.error_text(msg)))
     5.8 +                out_lines = result.out_lines ::: split_lines(Output.error_message_text(msg)))
     5.9            }
    5.10          }
    5.11          else {
    5.12 @@ -309,8 +309,8 @@
    5.13        timeout_request.foreach(_.cancel)
    5.14  
    5.15        if (result.interrupted) {
    5.16 -        if (was_timeout) result.error(Output.error_text("Timeout")).was_timeout
    5.17 -        else result.error(Output.error_text("Interrupt"))
    5.18 +        if (was_timeout) result.error(Output.error_message_text("Timeout")).was_timeout
    5.19 +        else result.error(Output.error_message_text("Interrupt"))
    5.20        }
    5.21        else result
    5.22      }
     6.1 --- a/src/Tools/jEdit/src/session_build.scala	Sun May 14 17:01:05 2017 +0200
     6.2 +++ b/src/Tools/jEdit/src/session_build.scala	Sun May 14 17:05:06 2017 +0200
     6.3 @@ -173,7 +173,7 @@
     6.4          try { ("", JEdit_Sessions.session_build(options, progress = progress)) }
     6.5          catch {
     6.6            case exn: Throwable =>
     6.7 -            (Output.error_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
     6.8 +            (Output.error_message_text(Exn.message(exn)) + "\n", Exn.return_code(exn, 2))
     6.9          }
    6.10  
    6.11        progress.echo(out + (if (rc == 0) "OK\n" else "Return code: " + rc + "\n"))