src/Pure/PIDE/command.scala
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 {