src/Pure/General/output.scala
author wenzelm
Sat Apr 09 16:16:05 2016 +0200 (2016-04-09)
changeset 62930 51ac6bc389e8
parent 62553 d2e0d626fb96
child 62938 79f41fbdf74a
permissions -rw-r--r--
shared output primitives of physical/virtual Pure;
wenzelm@57453
     1
/*  Title:      Pure/General/output.scala
wenzelm@57453
     2
    Module:     PIDE
wenzelm@56782
     3
    Author:     Makarius
wenzelm@56782
     4
wenzelm@62930
     5
Isabelle output channels.
wenzelm@56782
     6
*/
wenzelm@56782
     7
wenzelm@56782
     8
package isabelle
wenzelm@56782
     9
wenzelm@56782
    10
wenzelm@56782
    11
object Output
wenzelm@56782
    12
{
wenzelm@59671
    13
  def clean_yxml(msg: String): String =
wenzelm@59671
    14
    try { XML.content(YXML.parse_body(msg)) }
wenzelm@59671
    15
    catch { case ERROR(_) => msg }
wenzelm@56782
    16
wenzelm@59671
    17
  def writeln_text(msg: String): String = clean_yxml(msg)
wenzelm@59671
    18
  def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
wenzelm@59671
    19
  def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
wenzelm@59671
    20
wenzelm@62553
    21
  def writeln(msg: String, stdout: Boolean = false)
wenzelm@62553
    22
  {
wenzelm@62553
    23
    if (msg != "") {
wenzelm@62553
    24
      if (stdout) Console.println(writeln_text(msg))
wenzelm@62553
    25
      else Console.err.println(writeln_text(msg))
wenzelm@62553
    26
    }
wenzelm@62553
    27
  }
wenzelm@62553
    28
wenzelm@62553
    29
  def warning(msg: String, stdout: Boolean = false)
wenzelm@62553
    30
  {
wenzelm@62553
    31
    if (msg != "") {
wenzelm@62553
    32
      if (stdout) Console.println(warning_text(msg))
wenzelm@62553
    33
      else Console.err.println(warning_text(msg))
wenzelm@62553
    34
    }
wenzelm@62553
    35
  }
wenzelm@62553
    36
wenzelm@62553
    37
  def error_message(msg: String, stdout: Boolean = false)
wenzelm@62553
    38
  {
wenzelm@62553
    39
    if (msg != "") {
wenzelm@62553
    40
      if (stdout) Console.println(error_text(msg))
wenzelm@62553
    41
      else Console.err.println(error_text(msg))
wenzelm@62553
    42
    }
wenzelm@62553
    43
  }
wenzelm@56782
    44
}