diff -r 74872a13f628 -r 07a7544c0535 src/Tools/jEdit/src/isabelle_sidekick.scala
--- a/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Apr 06 13:34:22 2015 +0200
+++ b/src/Tools/jEdit/src/isabelle_sidekick.scala Mon Apr 06 14:09:31 2015 +0200
@@ -39,10 +39,18 @@
protected var _end = int_to_pos(range.stop)
override def getIcon: Icon = null
override def getShortString: String =
- "" +
- (if (keyword != "" && _name.startsWith(keyword))
- "" + HTML.encode(keyword) + "" + HTML.encode(_name.substring(keyword.length))
- else HTML.encode(_name)) + ""
+ {
+ val n = keyword.length
+ val s =
+ _name.indexOf(keyword) match {
+ case i if i >= 0 && n > 0 =>
+ HTML.encode(_name.substring(0, i)) +
+ "" + HTML.encode(keyword) + "" +
+ HTML.encode(_name.substring(i + n))
+ case _ => HTML.encode(_name)
+ }
+ "" + s + ""
+ }
override def getLongString: String = _name
override def getName: String = _name
override def setName(name: String) = _name = name