src/Tools/jEdit/src/completion_popup.scala
author wenzelm
Tue Aug 27 16:45:32 2013 +0200 (2013-08-27 ago)
changeset 53231 423e29f1f304
parent 53230 6589ff56cc3c
child 53232 4a3762693452
permissions -rw-r--r--
avoid complication and event duplication due to KeyEventInterceptor -- NB: popup has focus within root window, it is closed on loss of focus;
uniform JEdit_Lib.propagate_key;
wenzelm@53023
     1
/*  Title:      Tools/jEdit/src/completion_popup.scala
wenzelm@53023
     2
    Author:     Makarius
wenzelm@53023
     3
wenzelm@53023
     4
Completion popup based on javax.swing.PopupFactory.
wenzelm@53023
     5
*/
wenzelm@53023
     6
wenzelm@53023
     7
package isabelle.jedit
wenzelm@53023
     8
wenzelm@53023
     9
wenzelm@53023
    10
import isabelle._
wenzelm@53023
    11
wenzelm@53229
    12
import java.awt.{Font, Point, BorderLayout, Dimension}
wenzelm@53226
    13
import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
wenzelm@53228
    14
import javax.swing.{JPanel, JComponent, PopupFactory, SwingUtilities}
wenzelm@53023
    15
wenzelm@53023
    16
import scala.swing.{ListView, ScrollPane}
wenzelm@53023
    17
import scala.swing.event.MouseClicked
wenzelm@53023
    18
wenzelm@53023
    19
import org.gjt.sp.jedit.View
wenzelm@53228
    20
import org.gjt.sp.jedit.textarea.JEditTextArea
wenzelm@53023
    21
wenzelm@53023
    22
wenzelm@53023
    23
object Completion_Popup
wenzelm@53023
    24
{
wenzelm@53023
    25
  sealed case class Item(name: String, text: String)
wenzelm@53023
    26
  { override def toString: String = text }
wenzelm@53023
    27
wenzelm@53023
    28
  def apply(
wenzelm@53023
    29
    opt_view: Option[View],
wenzelm@53229
    30
    root: JComponent,
wenzelm@53229
    31
    popup_font: Font,
wenzelm@53023
    32
    screen_point: Point,
wenzelm@53023
    33
    items: List[Item],
wenzelm@53229
    34
    complete: Item => Unit,
wenzelm@53229
    35
    hidden: () => Unit): Completion_Popup =
wenzelm@53023
    36
  {
wenzelm@53023
    37
    Swing_Thread.require()
wenzelm@53023
    38
wenzelm@53023
    39
    require(!items.isEmpty)
wenzelm@53023
    40
wenzelm@53229
    41
    val completion =
wenzelm@53229
    42
      new Completion_Popup(opt_view, root, popup_font, screen_point, items, complete, hidden)
wenzelm@53023
    43
    completion.show_popup()
wenzelm@53023
    44
    completion
wenzelm@53023
    45
  }
wenzelm@53228
    46
wenzelm@53228
    47
  def input_text_area(text_area: JEditTextArea, evt: KeyEvent)
wenzelm@53228
    48
  {
wenzelm@53228
    49
    Swing_Thread.require()
wenzelm@53228
    50
wenzelm@53228
    51
    val buffer = text_area.getBuffer
wenzelm@53228
    52
    if (buffer.isEditable) {
wenzelm@53229
    53
      val view = text_area.getView
wenzelm@53228
    54
      val painter = text_area.getPainter
wenzelm@53228
    55
      val caret = text_area.getCaretPosition
wenzelm@53228
    56
wenzelm@53228
    57
      // FIXME
wenzelm@53228
    58
      def complete(item: Item) { }
wenzelm@53229
    59
wenzelm@53229
    60
      def hidden() { text_area.requestFocus }
wenzelm@53229
    61
wenzelm@53229
    62
      // FIXME
wenzelm@53228
    63
      val token_length = 0
wenzelm@53228
    64
      val items: List[Item] = Nil
wenzelm@53228
    65
wenzelm@53229
    66
      val popup_font =
wenzelm@53229
    67
        painter.getFont.deriveFont(
wenzelm@53229
    68
          (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
wenzelm@53229
    69
            max 10.0f)
wenzelm@53229
    70
wenzelm@53228
    71
      if (!items.isEmpty) {
wenzelm@53228
    72
        val location = text_area.offsetToXY(caret - token_length)
wenzelm@53228
    73
        if (location != null) {
wenzelm@53228
    74
          location.y = location.y + painter.getFontMetrics.getHeight
wenzelm@53228
    75
          SwingUtilities.convertPointToScreen(location, painter)
wenzelm@53229
    76
          apply(Some(view), view.getRootPane, popup_font, location, items, complete _, hidden _)
wenzelm@53228
    77
        }
wenzelm@53228
    78
      }
wenzelm@53228
    79
    }
wenzelm@53228
    80
  }
wenzelm@53023
    81
}
wenzelm@53023
    82
wenzelm@53023
    83
wenzelm@53023
    84
class Completion_Popup private(
wenzelm@53023
    85
  opt_view: Option[View],
wenzelm@53229
    86
  root: JComponent,
wenzelm@53229
    87
  popup_font: Font,
wenzelm@53023
    88
  screen_point: Point,
wenzelm@53023
    89
  items: List[Completion_Popup.Item],
wenzelm@53229
    90
  complete: Completion_Popup.Item => Unit,
wenzelm@53229
    91
  hidden: () => Unit) extends JPanel(new BorderLayout)
wenzelm@53023
    92
{
wenzelm@53023
    93
  completion =>
wenzelm@53023
    94
wenzelm@53023
    95
  Swing_Thread.require()
wenzelm@53023
    96
wenzelm@53023
    97
wenzelm@53023
    98
  /* list view */
wenzelm@53023
    99
wenzelm@53023
   100
  private val list_view = new ListView(items)
wenzelm@53023
   101
  {
wenzelm@53229
   102
    font = popup_font
wenzelm@53023
   103
  }
wenzelm@53023
   104
  list_view.selection.intervalMode = ListView.IntervalMode.Single
wenzelm@53023
   105
  list_view.peer.setFocusTraversalKeysEnabled(false)
wenzelm@53023
   106
  list_view.peer.setVisibleRowCount(items.length min 8)
wenzelm@53023
   107
  list_view.peer.setSelectedIndex(0)
wenzelm@53023
   108
wenzelm@53023
   109
  private def complete_selected(): Boolean =
wenzelm@53023
   110
  {
wenzelm@53023
   111
    list_view.selection.items.toList match {
wenzelm@53023
   112
      case item :: _ => complete(item); true
wenzelm@53023
   113
      case _ => false
wenzelm@53023
   114
    }
wenzelm@53023
   115
  }
wenzelm@53023
   116
wenzelm@53023
   117
  private def move_items(n: Int)
wenzelm@53023
   118
  {
wenzelm@53023
   119
    val i = list_view.peer.getSelectedIndex
wenzelm@53023
   120
    val j = ((i + n) min (items.length - 1)) max 0
wenzelm@53023
   121
    if (i != j) {
wenzelm@53023
   122
      list_view.peer.setSelectedIndex(j)
wenzelm@53023
   123
      list_view.peer.ensureIndexIsVisible(j)
wenzelm@53023
   124
    }
wenzelm@53023
   125
  }
wenzelm@53023
   126
wenzelm@53023
   127
  private def move_pages(n: Int)
wenzelm@53023
   128
  {
wenzelm@53023
   129
    val page_size = list_view.peer.getVisibleRowCount - 1
wenzelm@53023
   130
    move_items(page_size * n)
wenzelm@53023
   131
  }
wenzelm@53023
   132
wenzelm@53023
   133
wenzelm@53023
   134
  /* event handling */
wenzelm@53023
   135
wenzelm@53226
   136
  private val key_listener =
wenzelm@53226
   137
    JEdit_Lib.key_listener(
wenzelm@53226
   138
      workaround = false,
wenzelm@53226
   139
      key_pressed = (e: KeyEvent) =>
wenzelm@53226
   140
        {
wenzelm@53226
   141
          if (!e.isConsumed) {
wenzelm@53226
   142
            e.getKeyCode match {
wenzelm@53226
   143
              case KeyEvent.VK_TAB =>
wenzelm@53226
   144
                if (complete_selected()) e.consume
wenzelm@53226
   145
                hide_popup()
wenzelm@53226
   146
              case KeyEvent.VK_ESCAPE =>
wenzelm@53226
   147
                hide_popup()
wenzelm@53226
   148
                e.consume
wenzelm@53226
   149
              case KeyEvent.VK_UP => move_items(-1); e.consume
wenzelm@53226
   150
              case KeyEvent.VK_DOWN => move_items(1); e.consume
wenzelm@53226
   151
              case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume
wenzelm@53226
   152
              case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume
wenzelm@53226
   153
              case _ =>
wenzelm@53226
   154
                if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown)
wenzelm@53226
   155
                  hide_popup()
wenzelm@53226
   156
            }
wenzelm@53226
   157
          }
wenzelm@53231
   158
          opt_view.foreach(JEdit_Lib.propagate_key(_, e))
wenzelm@53226
   159
        },
wenzelm@53226
   160
      key_typed = (e: KeyEvent) =>
wenzelm@53226
   161
        {
wenzelm@53231
   162
          opt_view.foreach(JEdit_Lib.propagate_key(_, e))
wenzelm@53023
   163
        }
wenzelm@53226
   164
    )
wenzelm@53023
   165
wenzelm@53226
   166
  list_view.peer.addKeyListener(key_listener)
wenzelm@53023
   167
wenzelm@53023
   168
  list_view.peer.addMouseListener(new MouseAdapter {
wenzelm@53023
   169
    override def mouseClicked(e: MouseEvent) {
wenzelm@53023
   170
      if (complete_selected()) e.consume
wenzelm@53023
   171
      hide_popup()
wenzelm@53023
   172
    }
wenzelm@53023
   173
  })
wenzelm@53023
   174
wenzelm@53023
   175
  list_view.peer.addFocusListener(new FocusAdapter {
wenzelm@53023
   176
    override def focusLost(e: FocusEvent) { hide_popup() }
wenzelm@53023
   177
  })
wenzelm@53023
   178
wenzelm@53023
   179
wenzelm@53023
   180
  /* main content */
wenzelm@53023
   181
wenzelm@53023
   182
  override def getFocusTraversalKeysEnabled = false
wenzelm@53023
   183
wenzelm@53023
   184
  completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent])
wenzelm@53023
   185
wenzelm@53023
   186
wenzelm@53023
   187
  /* popup */
wenzelm@53023
   188
wenzelm@53023
   189
  private val popup =
wenzelm@53023
   190
  {
wenzelm@53023
   191
    val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
wenzelm@53023
   192
wenzelm@53230
   193
    val x0 = root.getLocationOnScreen.x
wenzelm@53230
   194
    val y0 = root.getLocationOnScreen.y
wenzelm@53230
   195
    val w0 = root.getWidth
wenzelm@53230
   196
    val h0 = root.getHeight
wenzelm@53023
   197
wenzelm@53230
   198
    val (w, h) =
wenzelm@53230
   199
    {
wenzelm@53230
   200
      val geometry = JEdit_Lib.window_geometry(completion, completion)
wenzelm@53230
   201
      val bounds = Rendering.popup_bounds
wenzelm@53230
   202
      val w = geometry.width min (screen_bounds.width * bounds).toInt min w0
wenzelm@53230
   203
      val h = geometry.height min (screen_bounds.height * bounds).toInt min h0
wenzelm@53230
   204
      (w, h)
wenzelm@53230
   205
    }
wenzelm@53230
   206
wenzelm@53230
   207
    val (x, y) =
wenzelm@53230
   208
    {
wenzelm@53230
   209
      val x1 = x0 + w0 - w
wenzelm@53230
   210
      val y1 = y0 + h0 - h
wenzelm@53230
   211
      val x2 = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
wenzelm@53230
   212
      val y2 = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
wenzelm@53230
   213
      ((x2 min x1) max x0, (y2 min y1) max y0)
wenzelm@53230
   214
    }
wenzelm@53023
   215
wenzelm@53023
   216
    completion.setSize(new Dimension(w, h))
wenzelm@53023
   217
    completion.setPreferredSize(new Dimension(w, h))
wenzelm@53229
   218
    PopupFactory.getSharedInstance.getPopup(root, completion, x, y)
wenzelm@53023
   219
  }
wenzelm@53023
   220
wenzelm@53023
   221
  def show_popup()
wenzelm@53023
   222
  {
wenzelm@53023
   223
    popup.show
wenzelm@53023
   224
    list_view.requestFocus
wenzelm@53023
   225
  }
wenzelm@53023
   226
wenzelm@53023
   227
  def hide_popup()
wenzelm@53023
   228
  {
wenzelm@53229
   229
    popup.hide
wenzelm@53229
   230
    hidden()
wenzelm@53023
   231
  }
wenzelm@53023
   232
}
wenzelm@53023
   233