Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
authorwenzelm
Wed Sep 22 22:39:17 2010 +0200 (2010-09-22)
changeset 3962253365ba766ac
parent 39621 20bba9cc4b51
child 39623 6aae022fde9b
Command.accumulate: refrain from adding tracing messages to markup tree -- potential scalability problem;
src/Pure/PIDE/command.scala
src/Pure/PIDE/isar_document.scala
     1.1 --- a/src/Pure/PIDE/command.scala	Wed Sep 22 22:25:21 2010 +0200
     1.2 +++ b/src/Pure/PIDE/command.scala	Wed Sep 22 22:39:17 2010 +0200
     1.3 @@ -60,10 +60,14 @@
     1.4            atts match {
     1.5              case Markup.Serial(i) =>
     1.6                val result = XML.Elem(Markup(name, Position.purge(atts)), body)
     1.7 +              val st0 = add_result(i, result)
     1.8                val st1 =
     1.9 -                (add_result(i, result) /: Isar_Document.message_positions(command, message))(
    1.10 -                  (st, range) => st.add_markup(Text.Info(range, result)))
    1.11 -              (st1 /: Isar_Document.message_reports(message))(_ accumulate _)
    1.12 +                if (Isar_Document.is_tracing(message)) st0
    1.13 +                else
    1.14 +                  (st0 /: Isar_Document.message_positions(command, message))(
    1.15 +                    (st, range) => st.add_markup(Text.Info(range, result)))
    1.16 +              val st2 = (st1 /: Isar_Document.message_reports(message))(_ accumulate _)
    1.17 +              st2
    1.18              case _ => System.err.println("Ignored message without serial number: " + message); this
    1.19            }
    1.20        }
     2.1 --- a/src/Pure/PIDE/isar_document.scala	Wed Sep 22 22:25:21 2010 +0200
     2.2 +++ b/src/Pure/PIDE/isar_document.scala	Wed Sep 22 22:39:17 2010 +0200
     2.3 @@ -72,6 +72,12 @@
     2.4  
     2.5    /* specific messages */
     2.6  
     2.7 +  def is_tracing(msg: XML.Tree): Boolean =
     2.8 +    msg match {
     2.9 +      case XML.Elem(Markup(Markup.TRACING, _), _) => true
    2.10 +      case _ => false
    2.11 +    }
    2.12 +
    2.13    def is_warning(msg: XML.Tree): Boolean =
    2.14      msg match {
    2.15        case XML.Elem(Markup(Markup.WARNING, _), _) => true