src/Pure/PIDE/command.scala
changeset 50500 c94bba7906d2
parent 50499 f496b2b7bafb
child 50501 6f41f1646617
--- a/src/Pure/PIDE/command.scala	Wed Dec 12 23:36:07 2012 +0100
+++ b/src/Pure/PIDE/command.scala	Thu Dec 13 13:52:18 2012 +0100
@@ -73,10 +73,10 @@
 
               val st0 = copy(results = results + (i -> message1))
               val st1 =
-                if (Protocol.is_tracing(message)) st0
-                else
+                if (Protocol.is_inlined(message))
                   (st0 /: Protocol.message_positions(command, message))(
                     (st, range) => st.add_markup(Text.Info(range, message2)))
+                else st0
 
               st1
             case _ => System.err.println("Ignored message without serial number: " + message); this