--- a/src/Pure/PIDE/command.scala Thu Feb 20 14:17:28 2014 +0100
+++ b/src/Pure/PIDE/command.scala Thu Feb 20 14:36:17 2014 +0100
@@ -94,14 +94,14 @@
.add_markup("", Text.Info(command.proper_range, elem)) // FIXME cumulation order!?
case _ =>
- java.lang.System.err.println("Ignored status message: " + msg)
+ System.err.println("Ignored status message: " + msg)
state
})
case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
(this /: msgs)((state, msg) =>
{
- def bad(): Unit = java.lang.System.err.println("Ignored report message: " + msg)
+ def bad(): Unit = System.err.println("Ignored report message: " + msg)
msg match {
case XML.Elem(Markup(name, atts @ Position.Reported(id, file_name, raw_range)), args)
@@ -147,7 +147,7 @@
st
case _ =>
- java.lang.System.err.println("Ignored message without serial number: " + message)
+ System.err.println("Ignored message without serial number: " + message)
this
}
}