isabelle: src/Pure/General/output.scala@d1ea37df7358 (annotated)

57453 77d13a98f1c8 clarified quasi-generic PIDE; wenzelm parents: 56831 diff changeset	1	/* Title: Pure/General/output.scala
77d13a98f1c8 clarified quasi-generic PIDE; wenzelm parents: 56831 diff changeset	2	Module: PIDE
56782 433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup); wenzelm parents: diff changeset	3	Author: Makarius
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup); wenzelm parents: diff changeset	4
56830 e760242101fc tuned signature -- channels for diagnostic output for system tools means stderr; wenzelm parents: 56782 diff changeset	5	Isabelle channels for diagnostic output.
56782 433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup); wenzelm parents: diff changeset	6	*/
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup); wenzelm parents: diff changeset	7
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup); wenzelm parents: diff changeset	8	package isabelle
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup); wenzelm parents: diff changeset	9
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup); wenzelm parents: diff changeset	10
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup); wenzelm parents: diff changeset	11	object Output
433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup); wenzelm parents: diff changeset	12	{
59671 9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML; wenzelm parents: 57453 diff changeset	13	def clean_yxml(msg: String): String =
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML; wenzelm parents: 57453 diff changeset	14	try { XML.content(YXML.parse_body(msg)) }
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML; wenzelm parents: 57453 diff changeset	15	catch { case ERROR(_) => msg }
56782 433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup); wenzelm parents: diff changeset	16
59671 9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML; wenzelm parents: 57453 diff changeset	17	def writeln_text(msg: String): String = clean_yxml(msg)
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML; wenzelm parents: 57453 diff changeset	18	def warning_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("### " + _))
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML; wenzelm parents: 57453 diff changeset	19	def error_text(msg: String): String = cat_lines(split_lines(clean_yxml(msg)).map("*** " + _))
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML; wenzelm parents: 57453 diff changeset	20
9715eb8e9408 more precise position information in Isabelle/Scala, with YXML markup as in Isabelle/ML; wenzelm parents: 57453 diff changeset	21	def writeln(msg: String) { Console.err.println(writeln_text(msg)) }
56831 e3ccf0809d51 prefer scala.Console with its support for thread-local redirection; wenzelm parents: 56830 diff changeset	22	def warning(msg: String) { Console.err.println(warning_text(msg)) }
e3ccf0809d51 prefer scala.Console with its support for thread-local redirection; wenzelm parents: 56830 diff changeset	23	def error_message(msg: String) { Console.err.println(error_text(msg)) }
56782 433cf57550fa more systematic Isabelle output, like in classic Isabelle/ML (without markup); wenzelm parents: diff changeset	24	}

author	wenzelm
	Sun, 14 Jun 2015 15:53:13 +0200
changeset 60469	d1ea37df7358
parent 59671	9715eb8e9408
child 62297	b886c0946308
permissions	-rw-r--r--