Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;

--- a/src/Pure/PIDE/command.scala	Wed Sep 22 22:25:21 2010 +0200
+++ b/src/Pure/PIDE/command.scala	Wed Sep 22 22:39:17 2010 +0200
@@ -60,10 +60,14 @@
           atts match {
             case Markup.Serial(i) =>
               val result = XML.Elem(Markup(name, Position.purge(atts)), body)
+              val st0 = add_result(i, result)
               val st1 =
-                (add_result(i, result) /: Isar_Document.message_positions(command, message))(
-                  (st, range) => st.add_markup(Text.Info(range, result)))
-              (st1 /: Isar_Document.message_reports(message))(_ accumulate _)
+                if (Isar_Document.is_tracing(message)) st0
+                else
+                  (st0 /: Isar_Document.message_positions(command, message))(
+                    (st, range) => st.add_markup(Text.Info(range, result)))
+              val st2 = (st1 /: Isar_Document.message_reports(message))(_ accumulate _)
+              st2
             case _ => System.err.println("Ignored message without serial number: " + message); this
           }
       }

--- a/src/Pure/PIDE/isar_document.scala	Wed Sep 22 22:25:21 2010 +0200
+++ b/src/Pure/PIDE/isar_document.scala	Wed Sep 22 22:39:17 2010 +0200
@@ -72,6 +72,12 @@
 
   /* specific messages */
 
+  def is_tracing(msg: XML.Tree): Boolean =
+    msg match {
+      case XML.Elem(Markup(Markup.TRACING, _), _) => true
+      case _ => false
+    }
+
   def is_warning(msg: XML.Tree): Boolean =
     msg match {
       case XML.Elem(Markup(Markup.WARNING, _), _) => true