more robust timing info: do not rely on order of markup;
authorwenzelm
Fri Mar 23 17:09:36 2018 +0100 (16 months ago)
changeset 67933604da273e18d
parent 67932 04352338f7f3
child 67934 5b0636910618
more robust timing info: do not rely on order of markup;
src/Pure/PIDE/rendering.scala
     1.1 --- a/src/Pure/PIDE/rendering.scala	Fri Mar 23 16:07:20 2018 +0100
     1.2 +++ b/src/Pure/PIDE/rendering.scala	Fri Mar 23 17:09:36 2018 +0100
     1.3 @@ -539,8 +539,18 @@
     1.4        if (range == r) copy(rev_infos = (important -> tree) :: rev_infos)
     1.5        else copy (range = r, rev_infos = List(important -> tree))
     1.6      }
     1.7 +
     1.8 +    def timing_info(tree: XML.Tree): Option[XML.Tree] =
     1.9 +      tree match {
    1.10 +        case XML.Elem(Markup(Markup.TIMING, _), _) =>
    1.11 +          if (timing.elapsed.seconds >= timing_threshold) Some(XML.Text(timing.message)) else None
    1.12 +        case _ => Some(tree)
    1.13 +      }
    1.14      def infos(important: Boolean): List[XML.Tree] =
    1.15 -      rev_infos.filter(p => p._1 == important).reverse.map(_._2)
    1.16 +      for {
    1.17 +        (is_important, tree) <- rev_infos.reverse if is_important == important
    1.18 +        tree1 <- timing_info(tree)
    1.19 +      } yield tree1
    1.20    }
    1.21  
    1.22    def perhaps_append_file(node_name: Document.Node.Name, name: String): String =
    1.23 @@ -568,11 +578,8 @@
    1.24                if (name == "") kind1
    1.25                else if (kind1 == "") quote(name)
    1.26                else kind1 + " " + quote(name)
    1.27 -            val txt2 =
    1.28 -              if (kind == Markup.COMMAND && info.timing.elapsed.seconds >= timing_threshold)
    1.29 -                "\n" + info.timing.message
    1.30 -              else ""
    1.31 -            Some(info + (r0, true, XML.Text(txt1 + txt2)))
    1.32 +            val info1 = info + (r0, true, XML.Text(txt1))
    1.33 +            Some(if (kind == Markup.COMMAND) info1 + (r0, true, XML.elem(Markup.TIMING)) else info1)
    1.34  
    1.35            case (info, Text.Info(r0, XML.Elem(Markup.Path(name), _))) =>
    1.36              val file = perhaps_append_file(snapshot.node_name, name)