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;
     1 /*  Title:      Pure/General/output.scala
     2     Module:     PIDE
     3     Author:     Makarius
     4 
     5 Isabelle output channels.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 object Output
    12 {
    13   def clean_yxml(msg: String): String =
    14     try { XML.content(YXML.parse_body(msg)) }
    15     catch { case ERROR(_) => msg }
    16 
    17   def writeln_text(msg: String): String = clean_yxml(msg)
    18   def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
    19   def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
    20 
    21   def writeln(msg: String, stdout: Boolean = false)
    22   {
    23     if (msg != "") {
    24       if (stdout) Console.println(writeln_text(msg))
    25       else Console.err.println(writeln_text(msg))
    26     }
    27   }
    28 
    29   def warning(msg: String, stdout: Boolean = false)
    30   {
    31     if (msg != "") {
    32       if (stdout) Console.println(warning_text(msg))
    33       else Console.err.println(warning_text(msg))
    34     }
    35   }
    36 
    37   def error_message(msg: String, stdout: Boolean = false)
    38   {
    39     if (msg != "") {
    40       if (stdout) Console.println(error_text(msg))
    41       else Console.err.println(error_text(msg))
    42     }
    43   }
    44 }