--- a/src/Tools/jEdit/src/rendering.scala Wed Apr 16 09:38:40 2014 +0200
+++ b/src/Tools/jEdit/src/rendering.scala Wed Apr 16 11:52:26 2014 +0200
@@ -468,7 +468,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 = Word.plain_words(kind)
+ val kind1 = Word.implode(Word.explode('_', kind))
val txt1 = kind1 + " " + quote(name)
val t = prev.info._1
val txt2 =