src/Tools/jEdit/src/rendering.scala
changeset 55977 ec4830499634
parent 55919 2eb8c13339a5
child 56063 38f13d055107
equal deleted inserted replaced
55976:43815ee659bc 55977:ec4830499634
   457         range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
   457         range, Text.Info(range, (Timing.zero, Vector.empty)), Rendering.tooltip_elements, _ =>
   458         {
   458         {
   459           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
   459           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
   460             Some(Text.Info(r, (t1 + t2, info)))
   460             Some(Text.Info(r, (t1 + t2, info)))
   461           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
   461           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
   462             val kind1 = space_explode('_', kind).mkString(" ")
   462             val kind1 = Library.plain_words(kind)
   463             val txt1 = kind1 + " " + quote(name)
   463             val txt1 = kind1 + " " + quote(name)
   464             val t = prev.info._1
   464             val t = prev.info._1
   465             val txt2 =
   465             val txt2 =
   466               if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
   466               if (kind == Markup.COMMAND && t.elapsed.seconds >= timing_threshold)
   467                 "\n" + t.message
   467                 "\n" + t.message