# HG changeset patch # User wenzelm # Date 1377616640 -7200 # Node ID 4a37626934529c4797b905919fa1ecd2a3732d1f # Parent 423e29f1f304e0e326b5851f9958796b4337db16 tuned signature; diff -r 423e29f1f304 -r 4a3762693452 src/Tools/jEdit/src/completion_popup.scala --- a/src/Tools/jEdit/src/completion_popup.scala Tue Aug 27 16:45:32 2013 +0200 +++ b/src/Tools/jEdit/src/completion_popup.scala Tue Aug 27 17:17:20 2013 +0200 @@ -25,25 +25,6 @@ sealed case class Item(name: String, text: String) { override def toString: String = text } - def apply( - opt_view: Option[View], - root: JComponent, - popup_font: Font, - screen_point: Point, - items: List[Item], - complete: Item => Unit, - hidden: () => Unit): Completion_Popup = - { - Swing_Thread.require() - - require(!items.isEmpty) - - val completion = - new Completion_Popup(opt_view, root, popup_font, screen_point, items, complete, hidden) - completion.show_popup() - completion - } - def input_text_area(text_area: JEditTextArea, evt: KeyEvent) { Swing_Thread.require() @@ -57,8 +38,6 @@ // FIXME def complete(item: Item) { } - def hidden() { text_area.requestFocus } - // FIXME val token_length = 0 val items: List[Item] = Nil @@ -73,26 +52,33 @@ if (location != null) { location.y = location.y + painter.getFontMetrics.getHeight SwingUtilities.convertPointToScreen(location, painter) - apply(Some(view), view.getRootPane, popup_font, location, items, complete _, hidden _) + new Completion_Popup(view.getRootPane, popup_font, location, items) { + override def propagate(evt: KeyEvent) { JEdit_Lib.propagate_key(view, evt) } + override def hidden() { text_area.requestFocus } + } } } } } } - class Completion_Popup private( - opt_view: Option[View], root: JComponent, popup_font: Font, screen_point: Point, - items: List[Completion_Popup.Item], - complete: Completion_Popup.Item => Unit, - hidden: () => Unit) extends JPanel(new BorderLayout) + items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout) { completion => Swing_Thread.require() + require(!items.isEmpty) + + + /* actions */ + + def complete(item: Completion_Popup.Item) { } + def propagate(evt: KeyEvent) { } + def hidden() { } /* list view */ @@ -155,12 +141,9 @@ hide_popup() } } - opt_view.foreach(JEdit_Lib.propagate_key(_, e)) + propagate(e) }, - key_typed = (e: KeyEvent) => - { - opt_view.foreach(JEdit_Lib.propagate_key(_, e)) - } + key_typed = propagate _ ) list_view.peer.addKeyListener(key_listener) @@ -218,16 +201,13 @@ PopupFactory.getSharedInstance.getPopup(root, completion, x, y) } - def show_popup() - { - popup.show - list_view.requestFocus - } - - def hide_popup() + private def hide_popup() { popup.hide hidden() } + + popup.show + list_view.requestFocus }