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