src/Pure/General/output.scala
author wenzelm
Tue, 10 Nov 2015 22:27:48 +0100
changeset 61622 8bb7848b3d47
parent 59671 9715eb8e9408
child 62297 b886c0946308
permissions -rw-r--r--
smart quoting of non-identifiers, e.g. jEdit actions;

/*  Title:      Pure/General/output.scala
    Module:     PIDE
    Author:     Makarius

Isabelle channels for diagnostic output.
*/

package isabelle


object Output
{
  def clean_yxml(msg: String): String =
    try { XML.content(YXML.parse_body(msg)) }
    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 writeln(msg: String) { Console.err.println(writeln_text(msg)) }
  def warning(msg: String) { Console.err.println(warning_text(msg)) }
  def error_message(msg: String) { Console.err.println(error_text(msg)) }
}