author | wenzelm |
Tue, 16 Nov 2010 22:40:45 +0100 | |
changeset 40572 | 2315c3daee74 |
parent 40571 | fbac01813bff |
child 40573 | 113ccf02d323 |
--- a/src/Pure/PIDE/command.scala Tue Nov 16 22:13:54 2010 +0100 +++ b/src/Pure/PIDE/command.scala Tue Nov 16 22:40:45 2010 +0100 @@ -54,7 +54,9 @@ val props = Position.purge(atts) val info = Text.Info[Any](range, XML.Elem(Markup(name, props), args)) state.add_markup(info) - case _ => System.err.println("Ignored report message: " + msg); state + case _ => + // FIXME System.err.println("Ignored report message: " + msg) + state }) case XML.Elem(Markup(name, atts), body) => atts match {