src/Tools/jEdit/src/isabelle_sidekick.scala
changeset 59933 07a7544c0535
parent 59286 ac74eedb910a
child 60272 4f72b00d9952
     1.1 --- a/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Apr 06 13:34:22 2015 +0200
     1.2 +++ b/src/Tools/jEdit/src/isabelle_sidekick.scala	Mon Apr 06 14:09:31 2015 +0200
     1.3 @@ -39,10 +39,18 @@
     1.4      protected var _end = int_to_pos(range.stop)
     1.5      override def getIcon: Icon = null
     1.6      override def getShortString: String =
     1.7 -      "<html><span style=\"" + css + "\">" +
     1.8 -      (if (keyword != "" && _name.startsWith(keyword))
     1.9 -        "<b>" + HTML.encode(keyword) + "</b>" + HTML.encode(_name.substring(keyword.length))
    1.10 -       else HTML.encode(_name)) + "</span></html>"
    1.11 +    {
    1.12 +      val n = keyword.length
    1.13 +      val s =
    1.14 +        _name.indexOf(keyword) match {
    1.15 +          case i if i >= 0 && n > 0 =>
    1.16 +            HTML.encode(_name.substring(0, i)) +
    1.17 +            "<b>" + HTML.encode(keyword) + "</b>" +
    1.18 +            HTML.encode(_name.substring(i + n))
    1.19 +          case _ => HTML.encode(_name)
    1.20 +        }
    1.21 +      "<html><span style=\"" + css + "\">" + s + "</span></html>"
    1.22 +    }
    1.23      override def getLongString: String = _name
    1.24      override def getName: String = _name
    1.25      override def setName(name: String) = _name = name