src/Pure/PIDE/command.scala
changeset 56782 433cf57550fa
parent 56746 d37a5d09a277
child 57615 df1b3452d71c
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Apr 29 13:29:05 2014 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Apr 29 13:32:13 2014 +0200
     1.3 @@ -179,14 +179,14 @@
     1.4                    add_status(markup).
     1.5                    add_markup(true, Symbol.Text_Chunk.Default, Text.Info(command.proper_range, elem))
     1.6                case _ =>
     1.7 -                System.err.println("Ignored status message: " + msg)
     1.8 +                Output.warning("Ignored status message: " + msg)
     1.9                  state
    1.10              })
    1.11  
    1.12          case XML.Elem(Markup(Markup.REPORT, _), msgs) =>
    1.13            (this /: msgs)((state, msg) =>
    1.14              {
    1.15 -              def bad(): Unit = System.err.println("Ignored report message: " + msg)
    1.16 +              def bad(): Unit = Output.warning("Ignored report message: " + msg)
    1.17  
    1.18                msg match {
    1.19                  case XML.Elem(
    1.20 @@ -238,7 +238,7 @@
    1.21                st
    1.22  
    1.23              case _ =>
    1.24 -              System.err.println("Ignored message without serial number: " + message)
    1.25 +              Output.warning("Ignored message without serial number: " + message)
    1.26                this
    1.27            }
    1.28      }