# HG changeset patch # User wenzelm # Date 1399320896 -7200 # Node ID 1435f0c771dcb0f8a050e48aba508798a5d2fd64 # Parent d06ff36b4fa7301eb0365733a0aa87b133f84ee0 some complication with ListView.Renderer to get tooltips; diff -r d06ff36b4fa7 -r 1435f0c771dc src/Tools/jEdit/src/find_dockable.scala --- a/src/Tools/jEdit/src/find_dockable.scala Mon May 05 20:10:33 2014 +0200 +++ b/src/Tools/jEdit/src/find_dockable.scala Mon May 05 22:14:56 2014 +0200 @@ -12,7 +12,7 @@ import java.awt.event.{ComponentEvent, ComponentAdapter, KeyEvent} import javax.swing.{JComponent, JTextField} -import scala.swing.{Button, Component, TextField, CheckBox, Label, +import scala.swing.{Button, Component, TextField, CheckBox, Label, ListView, ComboBox, TabbedPane, BorderPanel} import scala.swing.event.{SelectionChanged, ButtonClicked, Key, KeyPressed} @@ -186,11 +186,6 @@ /* print operation */ - private case class Print_Item(name: String, description: String) - { - override def toString: String = description - } - private val print_operation = new Find_Dockable.Operation(view) { /* query */ @@ -200,12 +195,9 @@ (snapshot, results, body) => pretty_text_area.update(snapshot, results, Pretty.separate(body))) - private var _selector_item: Option[Print_Item] = None - private var _selector = new ComboBox[Print_Item](Nil) - private def apply_query() { - query_operation.apply_query(List(_selector.selection.item.name)) + query_operation.apply_query(List(_selector.selection.item)) } private val query_label = new Label("Print:") @@ -213,13 +205,32 @@ def query: JComponent = _selector.peer.asInstanceOf[JComponent] - /* GUI page */ + /* items */ - private def update_selector() + case class Item(name: String, description: String) + + class Renderer(old_renderer: ListView.Renderer[String], items: List[Item]) + extends ListView.Renderer[String] { - val items = Print_Operation.print_operations(PIDE.session).map(p => Print_Item(p._1, p._2)) + def componentFor(list: ListView[_], + selected: Boolean, focused: Boolean, item: String, index: Int) = + { + val component = old_renderer.componentFor(list, selected, focused, item, index) + try { component.tooltip = items(index).description } + catch { case _: IndexOutOfBoundsException => } + component + } + } + + private var _selector_item: Option[String] = None + private var _selector = new ComboBox[String](Nil) + + private def set_selector() + { + val items = Print_Operation.print_operations(PIDE.session).map(p => Item(p._1, p._2)) + _selector = - new ComboBox(items) { + new ComboBox(items.map(_.name)) { _selector_item.foreach(item => selection.item = item) listenTo(selection) reactions += { @@ -228,8 +239,12 @@ apply_query() } } + _selector.renderer = new Renderer(_selector.renderer, items) } - update_selector() + set_selector() + + + /* GUI page */ private val apply_button = new Button("Apply") { tooltip = "Apply to current context" @@ -240,7 +255,7 @@ def select { - update_selector() + set_selector() control_panel.contents.clear control_panel.contents ++= List(query_label, _selector, apply_button, zoom) }