avoid spam;
authorwenzelm
Tue Nov 16 22:40:45 2010 +0100 (2010-11-16)
changeset 405722315c3daee74
parent 40571 fbac01813bff
child 40573 113ccf02d323
avoid spam;
src/Pure/PIDE/command.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Tue Nov 16 22:13:54 2010 +0100
     1.2 +++ b/src/Pure/PIDE/command.scala	Tue Nov 16 22:40:45 2010 +0100
     1.3 @@ -54,7 +54,9 @@
     1.4                  val props = Position.purge(atts)
     1.5                  val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args))
     1.6                  state.add_markup(info)
     1.7 -              case _ => System.err.println("Ignored report message: " + msg); state
     1.8 +              case _ =>
     1.9 +                // FIXME System.err.println("Ignored report message: " + msg)
    1.10 +                state
    1.11              })
    1.12          case XML.Elem(Markup(name, atts), body) =>
    1.13            atts match {