src/Pure/General/output.scala
author wenzelm
Sun Dec 10 20:29:00 2017 +0100 (18 months ago)
changeset 67178 70576478bda9
parent 65828 02dd430d80c5
permissions -rw-r--r--
avoid println with its extra CR on Windows;
wenzelm@57453
     1
/*  Title:      Pure/General/output.scala
wenzelm@56782
     2
    Author:     Makarius
wenzelm@56782
     3
wenzelm@62930
     4
Isabelle output channels.
wenzelm@56782
     5
*/
wenzelm@56782
     6
wenzelm@56782
     7
package isabelle
wenzelm@56782
     8
wenzelm@56782
     9
wenzelm@56782
    10
object Output
wenzelm@56782
    11
{
wenzelm@59671
    12
  def clean_yxml(msg: String): String =
wenzelm@62938
    13
    try { XML.content(Protocol_Message.clean_reports(YXML.parse_body(msg))) }
wenzelm@59671
    14
    catch { case ERROR(_) => msg }
wenzelm@56782
    15
wenzelm@59671
    16
  def writeln_text(msg: String): String = clean_yxml(msg)
wenzelm@65828
    17
wenzelm@65828
    18
  def warning_text(msg: String): String =
wenzelm@65828
    19
    cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
wenzelm@65828
    20
wenzelm@65828
    21
  def error_message_text(msg: String): String =
wenzelm@65828
    22
    cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
wenzelm@59671
    23
wenzelm@62553
    24
  def writeln(msg: String, stdout: Boolean = false)
wenzelm@62553
    25
  {
wenzelm@62553
    26
    if (msg != "") {
wenzelm@67178
    27
      if (stdout) Console.print(writeln_text(msg) + "\n")
wenzelm@67178
    28
      else Console.err.print(writeln_text(msg) + "\n")
wenzelm@62553
    29
    }
wenzelm@62553
    30
  }
wenzelm@62553
    31
wenzelm@62553
    32
  def warning(msg: String, stdout: Boolean = false)
wenzelm@62553
    33
  {
wenzelm@62553
    34
    if (msg != "") {
wenzelm@67178
    35
      if (stdout) Console.print(warning_text(msg) + "\n")
wenzelm@67178
    36
      else Console.err.print(warning_text(msg) + "\n")
wenzelm@62553
    37
    }
wenzelm@62553
    38
  }
wenzelm@62553
    39
wenzelm@62553
    40
  def error_message(msg: String, stdout: Boolean = false)
wenzelm@62553
    41
  {
wenzelm@62553
    42
    if (msg != "") {
wenzelm@67178
    43
      if (stdout) Console.print(error_message_text(msg) + "\n")
wenzelm@67178
    44
      else Console.err.print(error_message_text(msg) + "\n")
wenzelm@62553
    45
    }
wenzelm@62553
    46
  }
wenzelm@56782
    47
}