src/Tools/jEdit/src/completion_popup.scala
author wenzelm
Tue Aug 27 14:56:11 2013 +0200 (2013-08-27 ago)
changeset 53228 f6c6688961db
parent 53226 9cf8e2263ca7
child 53229 6ce8328d7912
permissions -rw-r--r--
some key event handling in the manner of SideKickBindings, SideKickCompletionPopup;
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@53023
    12
import java.awt.{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@53023
    30
    parent: JComponent,
wenzelm@53023
    31
    screen_point: Point,
wenzelm@53023
    32
    items: List[Item],
wenzelm@53023
    33
    complete: Item => Unit): Completion_Popup =
wenzelm@53023
    34
  {
wenzelm@53023
    35
    Swing_Thread.require()
wenzelm@53023
    36
wenzelm@53023
    37
    require(!items.isEmpty)
wenzelm@53023
    38
wenzelm@53023
    39
    val completion = new Completion_Popup(opt_view, parent, screen_point, items, complete)
wenzelm@53023
    40
    completion.show_popup()
wenzelm@53023
    41
    completion
wenzelm@53023
    42
  }
wenzelm@53228
    43
wenzelm@53228
    44
  def input_text_area(text_area: JEditTextArea, evt: KeyEvent)
wenzelm@53228
    45
  {
wenzelm@53228
    46
    Swing_Thread.require()
wenzelm@53228
    47
wenzelm@53228
    48
    val buffer = text_area.getBuffer
wenzelm@53228
    49
    if (buffer.isEditable) {
wenzelm@53228
    50
      val painter = text_area.getPainter
wenzelm@53228
    51
      val caret = text_area.getCaretPosition
wenzelm@53228
    52
wenzelm@53228
    53
      // FIXME
wenzelm@53228
    54
      def complete(item: Item) { }
wenzelm@53228
    55
      val token_length = 0
wenzelm@53228
    56
      val items: List[Item] = Nil
wenzelm@53228
    57
wenzelm@53228
    58
      if (!items.isEmpty) {
wenzelm@53228
    59
        val location = text_area.offsetToXY(caret - token_length)
wenzelm@53228
    60
        if (location != null) {
wenzelm@53228
    61
          location.y = location.y + painter.getFontMetrics.getHeight
wenzelm@53228
    62
          SwingUtilities.convertPointToScreen(location, painter)
wenzelm@53228
    63
          apply(Some(text_area.getView), painter, location, items, complete _)
wenzelm@53228
    64
        }
wenzelm@53228
    65
      }
wenzelm@53228
    66
    }
wenzelm@53228
    67
  }
wenzelm@53023
    68
}
wenzelm@53023
    69
wenzelm@53023
    70
wenzelm@53023
    71
class Completion_Popup private(
wenzelm@53023
    72
  opt_view: Option[View],
wenzelm@53023
    73
  parent: JComponent,
wenzelm@53023
    74
  screen_point: Point,
wenzelm@53023
    75
  items: List[Completion_Popup.Item],
wenzelm@53023
    76
  complete: Completion_Popup.Item => Unit) extends JPanel(new BorderLayout)
wenzelm@53023
    77
{
wenzelm@53023
    78
  completion =>
wenzelm@53023
    79
wenzelm@53023
    80
  Swing_Thread.require()
wenzelm@53023
    81
wenzelm@53023
    82
wenzelm@53023
    83
  /* list view */
wenzelm@53023
    84
wenzelm@53023
    85
  private val list_view = new ListView(items)
wenzelm@53023
    86
  {
wenzelm@53023
    87
    font = parent.getFont
wenzelm@53023
    88
  }
wenzelm@53023
    89
  list_view.selection.intervalMode = ListView.IntervalMode.Single
wenzelm@53023
    90
  list_view.peer.setFocusTraversalKeysEnabled(false)
wenzelm@53023
    91
  list_view.peer.setVisibleRowCount(items.length min 8)
wenzelm@53023
    92
  list_view.peer.setSelectedIndex(0)
wenzelm@53023
    93
wenzelm@53023
    94
  private def complete_selected(): Boolean =
wenzelm@53023
    95
  {
wenzelm@53023
    96
    list_view.selection.items.toList match {
wenzelm@53023
    97
      case item :: _ => complete(item); true
wenzelm@53023
    98
      case _ => false
wenzelm@53023
    99
    }
wenzelm@53023
   100
  }
wenzelm@53023
   101
wenzelm@53023
   102
  private def move_items(n: Int)
wenzelm@53023
   103
  {
wenzelm@53023
   104
    val i = list_view.peer.getSelectedIndex
wenzelm@53023
   105
    val j = ((i + n) min (items.length - 1)) max 0
wenzelm@53023
   106
    if (i != j) {
wenzelm@53023
   107
      list_view.peer.setSelectedIndex(j)
wenzelm@53023
   108
      list_view.peer.ensureIndexIsVisible(j)
wenzelm@53023
   109
    }
wenzelm@53023
   110
  }
wenzelm@53023
   111
wenzelm@53023
   112
  private def move_pages(n: Int)
wenzelm@53023
   113
  {
wenzelm@53023
   114
    val page_size = list_view.peer.getVisibleRowCount - 1
wenzelm@53023
   115
    move_items(page_size * n)
wenzelm@53023
   116
  }
wenzelm@53023
   117
wenzelm@53023
   118
wenzelm@53023
   119
  /* event handling */
wenzelm@53023
   120
wenzelm@53226
   121
  private val key_listener =
wenzelm@53226
   122
    JEdit_Lib.key_listener(
wenzelm@53226
   123
      workaround = false,
wenzelm@53226
   124
      key_pressed = (e: KeyEvent) =>
wenzelm@53226
   125
        {
wenzelm@53226
   126
          if (!e.isConsumed) {
wenzelm@53226
   127
            e.getKeyCode match {
wenzelm@53226
   128
              case KeyEvent.VK_TAB =>
wenzelm@53226
   129
                if (complete_selected()) e.consume
wenzelm@53226
   130
                hide_popup()
wenzelm@53226
   131
              case KeyEvent.VK_ESCAPE =>
wenzelm@53226
   132
                hide_popup()
wenzelm@53226
   133
                e.consume
wenzelm@53226
   134
              case KeyEvent.VK_UP => move_items(-1); e.consume
wenzelm@53226
   135
              case KeyEvent.VK_DOWN => move_items(1); e.consume
wenzelm@53226
   136
              case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume
wenzelm@53226
   137
              case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume
wenzelm@53226
   138
              case _ =>
wenzelm@53226
   139
                if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown)
wenzelm@53226
   140
                  hide_popup()
wenzelm@53226
   141
            }
wenzelm@53226
   142
          }
wenzelm@53226
   143
          if (!e.isConsumed) pass_to_view(e)
wenzelm@53226
   144
        },
wenzelm@53226
   145
      key_typed = (e: KeyEvent) =>
wenzelm@53226
   146
        {
wenzelm@53226
   147
          if (!e.isConsumed) pass_to_view(e)
wenzelm@53023
   148
        }
wenzelm@53226
   149
    )
wenzelm@53023
   150
wenzelm@53023
   151
  private def pass_to_view(e: KeyEvent)
wenzelm@53023
   152
  {
wenzelm@53023
   153
    opt_view match {
wenzelm@53226
   154
      case Some(view) if view.getKeyEventInterceptor == key_listener =>
wenzelm@53023
   155
        try {
wenzelm@53023
   156
          view.setKeyEventInterceptor(null)
wenzelm@53023
   157
          view.getInputHandler().processKeyEvent(e, View.ACTION_BAR, false)
wenzelm@53023
   158
        }
wenzelm@53226
   159
        finally { view.setKeyEventInterceptor(key_listener) }
wenzelm@53023
   160
      case _ =>
wenzelm@53023
   161
    }
wenzelm@53023
   162
  }
wenzelm@53023
   163
wenzelm@53226
   164
  list_view.peer.addKeyListener(key_listener)
wenzelm@53023
   165
wenzelm@53023
   166
  list_view.peer.addMouseListener(new MouseAdapter {
wenzelm@53023
   167
    override def mouseClicked(e: MouseEvent) {
wenzelm@53023
   168
      if (complete_selected()) e.consume
wenzelm@53023
   169
      hide_popup()
wenzelm@53023
   170
    }
wenzelm@53023
   171
  })
wenzelm@53023
   172
wenzelm@53023
   173
  list_view.peer.addFocusListener(new FocusAdapter {
wenzelm@53023
   174
    override def focusLost(e: FocusEvent) { hide_popup() }
wenzelm@53023
   175
  })
wenzelm@53023
   176
wenzelm@53023
   177
wenzelm@53023
   178
  /* main content */
wenzelm@53023
   179
wenzelm@53023
   180
  override def getFocusTraversalKeysEnabled = false
wenzelm@53023
   181
wenzelm@53023
   182
  completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent])
wenzelm@53023
   183
wenzelm@53023
   184
wenzelm@53023
   185
  /* popup */
wenzelm@53023
   186
wenzelm@53023
   187
  private val popup =
wenzelm@53023
   188
  {
wenzelm@53023
   189
    val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
wenzelm@53023
   190
wenzelm@53023
   191
    val geometry = JEdit_Lib.window_geometry(completion, completion)
wenzelm@53023
   192
wenzelm@53023
   193
    val w = geometry.width min (screen_bounds.width / 2)
wenzelm@53023
   194
    val h = geometry.height min (screen_bounds.height / 2)
wenzelm@53023
   195
wenzelm@53023
   196
    completion.setSize(new Dimension(w, h))
wenzelm@53023
   197
    completion.setPreferredSize(new Dimension(w, h))
wenzelm@53023
   198
wenzelm@53023
   199
    val x = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
wenzelm@53023
   200
    val y = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
wenzelm@53023
   201
    PopupFactory.getSharedInstance.getPopup(parent, completion, x, y)
wenzelm@53023
   202
  }
wenzelm@53023
   203
wenzelm@53023
   204
  def show_popup()
wenzelm@53023
   205
  {
wenzelm@53226
   206
    opt_view.foreach(view => view.setKeyEventInterceptor(key_listener))
wenzelm@53023
   207
    popup.show
wenzelm@53023
   208
    list_view.requestFocus
wenzelm@53023
   209
  }
wenzelm@53023
   210
wenzelm@53023
   211
  def hide_popup()
wenzelm@53023
   212
  {
wenzelm@53023
   213
    opt_view match {
wenzelm@53228
   214
      case Some(view) =>
wenzelm@53228
   215
        if (view.getKeyEventInterceptor == key_listener)
wenzelm@53228
   216
          view.setKeyEventInterceptor(null)
wenzelm@53228
   217
        popup.hide
wenzelm@53228
   218
        view.getTextArea match {
wenzelm@53228
   219
          case null =>
wenzelm@53228
   220
          case text_area => text_area.requestFocus
wenzelm@53228
   221
        }
wenzelm@53228
   222
      case None =>
wenzelm@53228
   223
        popup.hide
wenzelm@53228
   224
        parent.requestFocus
wenzelm@53023
   225
    }
wenzelm@53023
   226
  }
wenzelm@53023
   227
}
wenzelm@53023
   228