# HG changeset patch # User wenzelm # Date 1285187957 -7200 # Node ID 53365ba766acd771c0bfe76e6ced4e1664c21948 # Parent 20bba9cc4b519d852df11f7cbe45ffa0e1e405a3 Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem; diff -r 20bba9cc4b51 -r 53365ba766ac src/Pure/PIDE/command.scala --- 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 } } diff -r 20bba9cc4b51 -r 53365ba766ac src/Pure/PIDE/isar_document.scala --- 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