--- a/src/Pure/General/completion.scala Fri Mar 07 14:37:25 2014 +0100
+++ b/src/Pure/General/completion.scala Fri Mar 07 15:16:08 2014 +0100
@@ -21,11 +21,10 @@
range: Text.Range,
original: String,
name: String,
- description: String,
+ description: List[String],
replacement: String,
move: Int,
immediate: Boolean)
- { override def toString: String = description }
object Result
{
@@ -167,7 +166,7 @@
(full_name, descr_name) =
if (kind == "") (name, quote(decode(name)))
else (kind + "." + name, Library.plain_words(kind) + " " + quote(decode(name)))
- description = xname1 + " (" + descr_name + ")"
+ description = List(xname1, "(" + descr_name + ")")
} yield Item(range, original, full_name, description, xname1, 0, true)
if (items.isEmpty) None
@@ -377,13 +376,14 @@
case List(s1, s2) => (s1, s2)
case _ => (name1, "")
}
+ val move = - s2.length
val description =
- if (keywords(name)) name1 + " (keyword)"
+ if (move != 0) List(name1, "(template)")
+ else if (keywords(name)) List(name1, "(keyword)")
else if (Symbol.names.isDefinedAt(name) && name != name1)
- name1 + " (symbol " + quote(name) + ")"
- else name1
- Completion.Item(
- range, word, name1, description, s1 + s2, - s2.length, explicit || immediate)
+ List(name1, "(symbol " + quote(name) + ")")
+ else List(name1)
+ Completion.Item(range, word, name1, description, s1 + s2, move, explicit || immediate)
}
Some(Completion.Result(range, word, cs.length == 1, items.sorted(history.ordering)))
}
--- a/src/Tools/jEdit/src/completion_popup.scala Fri Mar 07 14:37:25 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala Fri Mar 07 15:16:08 2014 +0100
@@ -25,6 +25,22 @@
object Completion_Popup
{
+ /** items with HTML rendering **/
+
+ private class Item(val item: Completion.Item)
+ {
+ private val html =
+ item.description match {
+ case a :: bs =>
+ "<html><b>" + HTML.encode(a) + "</b>" +
+ HTML.encode(bs.map(" " + _).mkString) + "</html>"
+ case Nil => ""
+ }
+ override def toString: String = html
+ }
+
+
+
/** jEdit text area **/
object Text_Area
@@ -210,8 +226,10 @@
SwingUtilities.convertPoint(painter,
loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
+ val items = result.items.map(new Item(_))
val completion =
- new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, result.items) {
+ new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, items)
+ {
override def complete(item: Completion.Item) {
PIDE.completion_history.update(item)
insert(item)
@@ -402,18 +420,19 @@
val loc =
SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
+ val items = result.items.map(new Item(_))
val completion =
- new Completion_Popup(None, layered, loc, text_field.getFont, result.items)
- {
- override def complete(item: Completion.Item) {
- PIDE.completion_history.update(item)
- insert(item)
+ new Completion_Popup(None, layered, loc, text_field.getFont, items)
+ {
+ override def complete(item: Completion.Item) {
+ PIDE.completion_history.update(item)
+ insert(item)
+ }
+ override def propagate(evt: KeyEvent) {
+ if (!evt.isConsumed) text_field.processKeyEvent(evt)
+ }
+ override def refocus() { text_field.requestFocus }
}
- override def propagate(evt: KeyEvent) {
- if (!evt.isConsumed) text_field.processKeyEvent(evt)
- }
- override def refocus() { text_field.requestFocus }
- }
completion_popup = Some(completion)
completion.show_popup()
@@ -474,7 +493,7 @@
layered: JLayeredPane,
location: Point,
font: Font,
- items: List[Completion.Item]) extends JPanel(new BorderLayout)
+ items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
{
completion =>
@@ -508,7 +527,7 @@
private def complete_selected(): Boolean =
{
list_view.selection.items.toList match {
- case item :: _ => complete(item); true
+ case item :: _ => complete(item.item); true
case _ => false
}
}