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