equal
deleted
inserted
replaced
46 HTML.output(_name.substring(0, i)) + |
46 HTML.output(_name.substring(0, i)) + |
47 "<b>" + HTML.output(keyword) + "</b>" + |
47 "<b>" + HTML.output(keyword) + "</b>" + |
48 HTML.output(_name.substring(i + n)) |
48 HTML.output(_name.substring(i + n)) |
49 case _ => HTML.output(_name) |
49 case _ => HTML.output(_name) |
50 } |
50 } |
51 "<html><span style=\"" + css + "\">" + s + "</span></html>" |
51 GUI.Style_HTML.enclose_style(css, s) |
52 } |
52 } |
53 override def getLongString: String = _name |
53 override def getLongString: String = _name |
54 override def getName: String = _name |
54 override def getName: String = _name |
55 override def setName(name: String): Unit = _name = name |
55 override def setName(name: String): Unit = _name = name |
56 override def getStart: Position = _start |
56 override def getStart: Position = _start |