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