changeset 40572 | 2315c3daee74 |
parent 40454 | 2516ea25a54b |
child 43520 | cec9b95fa35d |
--- 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 {