src/Tools/jEdit/src/rendering.scala
changeset 55977 ec4830499634
parent 55919 2eb8c13339a5
child 56063 38f13d055107
--- a/src/Tools/jEdit/src/rendering.scala	Fri Mar 07 13:29:10 2014 +0100
+++ b/src/Tools/jEdit/src/rendering.scala	Fri Mar 07 14:37:25 2014 +0100
@@ -459,7 +459,7 @@
           case (Text.Info(r, (t1, info)), Text.Info(_, XML.Elem(Markup.Timing(t2), _))) =>
             Some(Text.Info(r, (t1 + t2, info)))
           case (prev, Text.Info(r, XML.Elem(Markup.Entity(kind, name), _))) =>
-            val kind1 = space_explode('_', kind).mkString(" ")
+            val kind1 = Library.plain_words(kind)
             val txt1 = kind1 + " " + quote(name)
             val t = prev.info._1
             val txt2 =