src/Tools/jEdit/src/completion_popup.scala
changeset 53232 4a3762693452
parent 53231 423e29f1f304
child 53233 4b422e5d64fd
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 16:45:32 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Aug 27 17:17:20 2013 +0200
     1.3 @@ -25,25 +25,6 @@
     1.4    sealed case class Item(name: String, text: String)
     1.5    { override def toString: String = text }
     1.6  
     1.7 -  def apply(
     1.8 -    opt_view: Option[View],
     1.9 -    root: JComponent,
    1.10 -    popup_font: Font,
    1.11 -    screen_point: Point,
    1.12 -    items: List[Item],
    1.13 -    complete: Item => Unit,
    1.14 -    hidden: () => Unit): Completion_Popup =
    1.15 -  {
    1.16 -    Swing_Thread.require()
    1.17 -
    1.18 -    require(!items.isEmpty)
    1.19 -
    1.20 -    val completion =
    1.21 -      new Completion_Popup(opt_view, root, popup_font, screen_point, items, complete, hidden)
    1.22 -    completion.show_popup()
    1.23 -    completion
    1.24 -  }
    1.25 -
    1.26    def input_text_area(text_area: JEditTextArea, evt: KeyEvent)
    1.27    {
    1.28      Swing_Thread.require()
    1.29 @@ -57,8 +38,6 @@
    1.30        // FIXME
    1.31        def complete(item: Item) { }
    1.32  
    1.33 -      def hidden() { text_area.requestFocus }
    1.34 -
    1.35        // FIXME
    1.36        val token_length = 0
    1.37        val items: List[Item] = Nil
    1.38 @@ -73,26 +52,33 @@
    1.39          if (location != null) {
    1.40            location.y = location.y + painter.getFontMetrics.getHeight
    1.41            SwingUtilities.convertPointToScreen(location, painter)
    1.42 -          apply(Some(view), view.getRootPane, popup_font, location, items, complete _, hidden _)
    1.43 +          new Completion_Popup(view.getRootPane, popup_font, location, items) {
    1.44 +            override def propagate(evt: KeyEvent) { JEdit_Lib.propagate_key(view, evt) }
    1.45 +            override def hidden() { text_area.requestFocus }
    1.46 +          }
    1.47          }
    1.48        }
    1.49      }
    1.50    }
    1.51  }
    1.52  
    1.53 -
    1.54  class Completion_Popup private(
    1.55 -  opt_view: Option[View],
    1.56    root: JComponent,
    1.57    popup_font: Font,
    1.58    screen_point: Point,
    1.59 -  items: List[Completion_Popup.Item],
    1.60 -  complete: Completion_Popup.Item => Unit,
    1.61 -  hidden: () => Unit) extends JPanel(new BorderLayout)
    1.62 +  items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
    1.63  {
    1.64    completion =>
    1.65  
    1.66    Swing_Thread.require()
    1.67 +  require(!items.isEmpty)
    1.68 +
    1.69 +
    1.70 +  /* actions */
    1.71 +
    1.72 +  def complete(item: Completion_Popup.Item) { }
    1.73 +  def propagate(evt: KeyEvent) { }
    1.74 +  def hidden() { }
    1.75  
    1.76  
    1.77    /* list view */
    1.78 @@ -155,12 +141,9 @@
    1.79                    hide_popup()
    1.80              }
    1.81            }
    1.82 -          opt_view.foreach(JEdit_Lib.propagate_key(_, e))
    1.83 +          propagate(e)
    1.84          },
    1.85 -      key_typed = (e: KeyEvent) =>
    1.86 -        {
    1.87 -          opt_view.foreach(JEdit_Lib.propagate_key(_, e))
    1.88 -        }
    1.89 +      key_typed = propagate _
    1.90      )
    1.91  
    1.92    list_view.peer.addKeyListener(key_listener)
    1.93 @@ -218,16 +201,13 @@
    1.94      PopupFactory.getSharedInstance.getPopup(root, completion, x, y)
    1.95    }
    1.96  
    1.97 -  def show_popup()
    1.98 -  {
    1.99 -    popup.show
   1.100 -    list_view.requestFocus
   1.101 -  }
   1.102 -
   1.103 -  def hide_popup()
   1.104 +  private def hide_popup()
   1.105    {
   1.106      popup.hide
   1.107      hidden()
   1.108    }
   1.109 +
   1.110 +  popup.show
   1.111 +  list_view.requestFocus
   1.112  }
   1.113