--- a/src/Pure/PIDE/command.scala Tue Apr 29 13:29:05 2014 +0200
+++ b/src/Pure/PIDE/command.scala Tue Apr 29 13:32:13 2014 +0200
@@ -179,14 +179,14 @@
add_status(markup).
add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem))
case _ =>
- System.err.println("Ignored status message: " + msg)
+ Output.warning("Ignored status message: " + msg)
state
})
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
{
- def bad(): Unit = System.err.println("Ignored report message: " + msg)
+ def bad(): Unit = Output.warning("Ignored report message: " + msg)
msg match {
case XML.Elem(
@@ -238,7 +238,7 @@
st
case _ =>
- System.err.println("Ignored message without serial number: " + message)
+ Output.warning("Ignored message without serial number: " + message)
this
}
}