src/Tools/jEdit/src/completion_popup.scala
author wenzelm
Tue Aug 27 12:35:32 2013 +0200 (2013-08-27 ago)
changeset 53226 9cf8e2263ca7
parent 53023 f127e949389f
child 53228 f6c6688961db
permissions -rw-r--r--
more systematic JEdit_Lib.key_listener with optional KeyEventWorkaround;
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@53023
    14
import javax.swing.{JPanel, JComponent, PopupFactory}
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@53226
    20
import org.gjt.sp.jedit.gui.KeyEventWorkaround
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@53023
    43
}
wenzelm@53023
    44
wenzelm@53023
    45
wenzelm@53023
    46
class Completion_Popup private(
wenzelm@53023
    47
  opt_view: Option[View],
wenzelm@53023
    48
  parent: JComponent,
wenzelm@53023
    49
  screen_point: Point,
wenzelm@53023
    50
  items: List[Completion_Popup.Item],
wenzelm@53023
    51
  complete: Completion_Popup.Item => Unit) extends JPanel(new BorderLayout)
wenzelm@53023
    52
{
wenzelm@53023
    53
  completion =>
wenzelm@53023
    54
wenzelm@53023
    55
  Swing_Thread.require()
wenzelm@53023
    56
wenzelm@53023
    57
wenzelm@53023
    58
  /* list view */
wenzelm@53023
    59
wenzelm@53023
    60
  private val list_view = new ListView(items)
wenzelm@53023
    61
  {
wenzelm@53023
    62
    font = parent.getFont
wenzelm@53023
    63
  }
wenzelm@53023
    64
  list_view.selection.intervalMode = ListView.IntervalMode.Single
wenzelm@53023
    65
  list_view.peer.setFocusTraversalKeysEnabled(false)
wenzelm@53023
    66
  list_view.peer.setVisibleRowCount(items.length min 8)
wenzelm@53023
    67
  list_view.peer.setSelectedIndex(0)
wenzelm@53023
    68
wenzelm@53023
    69
  private def complete_selected(): Boolean =
wenzelm@53023
    70
  {
wenzelm@53023
    71
    list_view.selection.items.toList match {
wenzelm@53023
    72
      case item :: _ => complete(item); true
wenzelm@53023
    73
      case _ => false
wenzelm@53023
    74
    }
wenzelm@53023
    75
  }
wenzelm@53023
    76
wenzelm@53023
    77
  private def move_items(n: Int)
wenzelm@53023
    78
  {
wenzelm@53023
    79
    val i = list_view.peer.getSelectedIndex
wenzelm@53023
    80
    val j = ((i + n) min (items.length - 1)) max 0
wenzelm@53023
    81
    if (i != j) {
wenzelm@53023
    82
      list_view.peer.setSelectedIndex(j)
wenzelm@53023
    83
      list_view.peer.ensureIndexIsVisible(j)
wenzelm@53023
    84
    }
wenzelm@53023
    85
  }
wenzelm@53023
    86
wenzelm@53023
    87
  private def move_pages(n: Int)
wenzelm@53023
    88
  {
wenzelm@53023
    89
    val page_size = list_view.peer.getVisibleRowCount - 1
wenzelm@53023
    90
    move_items(page_size * n)
wenzelm@53023
    91
  }
wenzelm@53023
    92
wenzelm@53023
    93
wenzelm@53023
    94
  /* event handling */
wenzelm@53023
    95
wenzelm@53226
    96
  private val key_listener =
wenzelm@53226
    97
    JEdit_Lib.key_listener(
wenzelm@53226
    98
      workaround = false,
wenzelm@53226
    99
      key_pressed = (e: KeyEvent) =>
wenzelm@53226
   100
        {
wenzelm@53226
   101
          if (!e.isConsumed) {
wenzelm@53226
   102
            e.getKeyCode match {
wenzelm@53226
   103
              case KeyEvent.VK_TAB =>
wenzelm@53226
   104
                if (complete_selected()) e.consume
wenzelm@53226
   105
                hide_popup()
wenzelm@53226
   106
              case KeyEvent.VK_ESCAPE =>
wenzelm@53226
   107
                hide_popup()
wenzelm@53226
   108
                e.consume
wenzelm@53226
   109
              case KeyEvent.VK_UP => move_items(-1); e.consume
wenzelm@53226
   110
              case KeyEvent.VK_DOWN => move_items(1); e.consume
wenzelm@53226
   111
              case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume
wenzelm@53226
   112
              case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume
wenzelm@53226
   113
              case _ =>
wenzelm@53226
   114
                if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown)
wenzelm@53226
   115
                  hide_popup()
wenzelm@53226
   116
            }
wenzelm@53226
   117
          }
wenzelm@53226
   118
          if (!e.isConsumed) pass_to_view(e)
wenzelm@53226
   119
        },
wenzelm@53226
   120
      key_typed = (e: KeyEvent) =>
wenzelm@53226
   121
        {
wenzelm@53226
   122
          if (!e.isConsumed) pass_to_view(e)
wenzelm@53023
   123
        }
wenzelm@53226
   124
    )
wenzelm@53023
   125
wenzelm@53023
   126
  private def pass_to_view(e: KeyEvent)
wenzelm@53023
   127
  {
wenzelm@53023
   128
    opt_view match {
wenzelm@53226
   129
      case Some(view) if view.getKeyEventInterceptor == key_listener =>
wenzelm@53023
   130
        try {
wenzelm@53023
   131
          view.setKeyEventInterceptor(null)
wenzelm@53023
   132
          view.getInputHandler().processKeyEvent(e, View.ACTION_BAR, false)
wenzelm@53023
   133
        }
wenzelm@53226
   134
        finally { view.setKeyEventInterceptor(key_listener) }
wenzelm@53023
   135
      case _ =>
wenzelm@53023
   136
    }
wenzelm@53023
   137
  }
wenzelm@53023
   138
wenzelm@53226
   139
  list_view.peer.addKeyListener(key_listener)
wenzelm@53023
   140
wenzelm@53023
   141
  list_view.peer.addMouseListener(new MouseAdapter {
wenzelm@53023
   142
    override def mouseClicked(e: MouseEvent) {
wenzelm@53023
   143
      if (complete_selected()) e.consume
wenzelm@53023
   144
      hide_popup()
wenzelm@53023
   145
    }
wenzelm@53023
   146
  })
wenzelm@53023
   147
wenzelm@53023
   148
  list_view.peer.addFocusListener(new FocusAdapter {
wenzelm@53023
   149
    override def focusLost(e: FocusEvent) { hide_popup() }
wenzelm@53023
   150
  })
wenzelm@53023
   151
wenzelm@53023
   152
wenzelm@53023
   153
  /* main content */
wenzelm@53023
   154
wenzelm@53023
   155
  override def getFocusTraversalKeysEnabled = false
wenzelm@53023
   156
wenzelm@53023
   157
  completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent])
wenzelm@53023
   158
wenzelm@53023
   159
wenzelm@53023
   160
  /* popup */
wenzelm@53023
   161
wenzelm@53023
   162
  private val popup =
wenzelm@53023
   163
  {
wenzelm@53023
   164
    val screen_bounds = JEdit_Lib.screen_bounds(screen_point)
wenzelm@53023
   165
wenzelm@53023
   166
    val geometry = JEdit_Lib.window_geometry(completion, completion)
wenzelm@53023
   167
wenzelm@53023
   168
    val w = geometry.width min (screen_bounds.width / 2)
wenzelm@53023
   169
    val h = geometry.height min (screen_bounds.height / 2)
wenzelm@53023
   170
wenzelm@53023
   171
    completion.setSize(new Dimension(w, h))
wenzelm@53023
   172
    completion.setPreferredSize(new Dimension(w, h))
wenzelm@53023
   173
wenzelm@53023
   174
    val x = screen_point.x min (screen_bounds.x + screen_bounds.width - w)
wenzelm@53023
   175
    val y = screen_point.y min (screen_bounds.y + screen_bounds.height - h)
wenzelm@53023
   176
    PopupFactory.getSharedInstance.getPopup(parent, completion, x, y)
wenzelm@53023
   177
  }
wenzelm@53023
   178
wenzelm@53023
   179
  def show_popup()
wenzelm@53023
   180
  {
wenzelm@53226
   181
    opt_view.foreach(view => view.setKeyEventInterceptor(key_listener))
wenzelm@53023
   182
    popup.show
wenzelm@53023
   183
    list_view.requestFocus
wenzelm@53023
   184
  }
wenzelm@53023
   185
wenzelm@53023
   186
  def hide_popup()
wenzelm@53023
   187
  {
wenzelm@53023
   188
    opt_view match {
wenzelm@53226
   189
      case Some(view) if view.getKeyEventInterceptor == key_listener =>
wenzelm@53023
   190
        view.setKeyEventInterceptor(null)
wenzelm@53023
   191
      case _ =>
wenzelm@53023
   192
    }
wenzelm@53023
   193
    popup.hide
wenzelm@53023
   194
    parent.requestFocus
wenzelm@53023
   195
  }
wenzelm@53023
   196
}
wenzelm@53023
   197