src/Tools/jEdit/src/rendering.scala
changeset 51588 167e2d64327a
parent 51574 2b58d7b139d6
child 52081 29566b6810f7
     1.1 --- a/src/Tools/jEdit/src/rendering.scala	Sat Mar 30 16:15:26 2013 +0100
     1.2 +++ b/src/Tools/jEdit/src/rendering.scala	Sat Mar 30 16:16:24 2013 +0100
     1.3 @@ -320,27 +320,39 @@
     1.4        Markup.DOCUMENT_SOURCE -> "document source")
     1.5  
     1.6    private val tooltip_elements =
     1.7 -    Set(Markup.ENTITY, Markup.SORTING, Markup.TYPING, Markup.ML_TYPING, Markup.PATH) ++
     1.8 -      tooltips.keys
     1.9 +    Set(Markup.TIMING, Markup.ENTITY, Markup.SORTING, Markup.TYPING,
    1.10 +      Markup.ML_TYPING, Markup.PATH) ++ tooltips.keys
    1.11  
    1.12    private def pretty_typing(kind: String, body: XML.Body): XML.Tree =
    1.13      Pretty.block(XML.Text(kind) :: Pretty.Break(1) :: body)
    1.14  
    1.15 +  private val timing_threshold: Double = options.real("jedit_timing_threshold")
    1.16 +
    1.17    def tooltip(range: Text.Range): Option[Text.Info[XML.Body]] =
    1.18    {
    1.19 -    def add(prev: Text.Info[List[(Boolean, XML.Tree)]], r0: Text.Range, p: (Boolean, XML.Tree)) =
    1.20 +    def add(prev: Text.Info[(Timing, List[(Boolean, XML.Tree)])],
    1.21 +      r0: Text.Range, p: (Boolean, XML.Tree)): Text.Info[(Timing, List[(Boolean, XML.Tree)])] =
    1.22      {
    1.23        val r = snapshot.convert(r0)
    1.24 -      if (prev.range == r) Text.Info(r, p :: prev.info) else Text.Info(r, List(p))
    1.25 +      val (t, info) = prev.info
    1.26 +      if (prev.range == r) Text.Info(r, (t, p :: info)) else Text.Info(r, (t, List(p)))
    1.27      }
    1.28  
    1.29      val results =
    1.30 -      snapshot.cumulate_markup[Text.Info[(List[(Boolean, XML.Tree)])]](
    1.31 -        range, Text.Info(range, Nil), Some(tooltip_elements), _ =>
    1.32 +      snapshot.cumulate_markup[Text.Info[(Timing, List[(Boolean, XML.Tree)])]](
    1.33 +        range, Text.Info(range, (Timing.zero, Nil)), Some(tooltip_elements), _ =>
    1.34          {
    1.35 +          case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
    1.36 +            Text.Info(r, (t1 + t2, info))
    1.37            case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
    1.38              val kind1 = space_explode('_', kind).mkString(" ")
    1.39 -            add(prev, r, (true, XML.Text(kind1 + " " + quote(name))))
    1.40 +            val txt1 = kind1 + " " + quote(name)
    1.41 +            val t = prev.info._1
    1.42 +            val txt2 =
    1.43 +              if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
    1.44 +                "\n" + t.message
    1.45 +              else ""
    1.46 +            add(prev, r, (true, XML.Text(txt1 + txt2)))
    1.47            case (prev, Text.Info(r, XML.Elem(Markup.Path(name), _)))
    1.48            if Path.is_ok(name) =>
    1.49              val jedit_file = PIDE.thy_load.append(snapshot.node_name.dir, Path.explode(name))
    1.50 @@ -351,10 +363,11 @@
    1.51            case (prev, Text.Info(r, XML.Elem(Markup(Markup.ML_TYPING, _), body))) =>
    1.52              add(prev, r, (false, pretty_typing("ML:", body)))
    1.53            case (prev, Text.Info(r, XML.Elem(Markup(name, _), _)))
    1.54 -          if tooltips.isDefinedAt(name) => add(prev, r, (true, XML.Text(tooltips(name))))
    1.55 +          if tooltips.isDefinedAt(name) =>
    1.56 +            add(prev, r, (true, XML.Text(tooltips(name))))
    1.57          }).toList.map(_.info)
    1.58  
    1.59 -    results.flatMap(_.info) match {
    1.60 +    results.map(_.info).flatMap(_._2) match {
    1.61        case Nil => None
    1.62        case tips =>
    1.63          val r = Text.Range(results.head.range.start, results.last.range.stop)