src/Pure/General/output.scala
changeset 56782 433cf57550fa
child 56830 e760242101fc
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/output.scala	Tue Apr 29 13:32:13 2014 +0200
@@ -0,0 +1,18 @@
+/*  Title:      Pure/General/output.ML
+    Author:     Makarius
+
+Isabelle output channels: plain text without markup.
+*/
+
+package isabelle
+
+
+object Output
+{
+  def warning_text(msg: String): String = cat_lines(split_lines(msg).map("### " + _))
+  def error_text(msg: String): String = cat_lines(split_lines(msg).map("*** " + _))
+
+  def warning(msg: String) { System.err.println(warning_text(msg)) }
+  def error_message(msg: String) { System.err.println(error_text(msg)) }
+}
+