src/Tools/jEdit/src/completion_popup.scala
author wenzelm
Thu Aug 29 13:00:59 2013 +0200 (2013-08-29 ago)
changeset 53275 b34aac6511ab
parent 53274 1760c01f1c78
child 53292 f567c1c7b180
permissions -rw-r--r--
tuned signature;
     1 /*  Title:      Tools/jEdit/src/completion_popup.scala
     2     Author:     Makarius
     3 
     4 Completion popup.
     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, JLayeredPane, 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   /* setup for jEdit text area */
    26 
    27   object Text_Area
    28   {
    29     private val key = new Object
    30 
    31     def apply(text_area: JEditTextArea): Option[Completion_Popup.Text_Area] =
    32       text_area.getClientProperty(key) match {
    33         case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
    34         case _ => None
    35       }
    36 
    37     def exit(text_area: JEditTextArea)
    38     {
    39       Swing_Thread.require()
    40       apply(text_area) match {
    41         case None =>
    42         case Some(text_area_completion) =>
    43           text_area_completion.deactivate()
    44           text_area.putClientProperty(key, null)
    45       }
    46     }
    47 
    48     def init(text_area: JEditTextArea): Completion_Popup.Text_Area =
    49     {
    50       exit(text_area)
    51       val text_area_completion = new Text_Area(text_area)
    52       text_area.putClientProperty(key, text_area_completion)
    53       text_area_completion.activate()
    54       text_area_completion
    55     }
    56 
    57     def dismissed(text_area: JEditTextArea): Boolean =
    58     {
    59       Swing_Thread.require()
    60       apply(text_area) match {
    61         case Some(text_area_completion) => text_area_completion.dismissed()
    62         case None => false
    63       }
    64     }
    65   }
    66 
    67   class Text_Area private(text_area: JEditTextArea)
    68   {
    69     /* popup state */
    70 
    71     private var completion_popup: Option[Completion_Popup] = None
    72 
    73     def dismissed(): Boolean =
    74     {
    75       Swing_Thread.require()
    76 
    77       completion_popup match {
    78         case Some(completion) =>
    79           completion.hide_popup()
    80           completion_popup = None
    81           true
    82         case None =>
    83           false
    84       }
    85     }
    86 
    87 
    88     /* insert selected item */
    89 
    90     private def insert(item: Completion.Item)
    91     {
    92       Swing_Thread.require()
    93 
    94       val buffer = text_area.getBuffer
    95       val len = item.original.length
    96       if (buffer.isEditable && len > 0) {
    97         JEdit_Lib.buffer_edit(buffer) {
    98           val caret = text_area.getCaretPosition
    99           JEdit_Lib.try_get_text(buffer, Text.Range(caret - len, caret)) match {
   100             case Some(text) if text == item.original =>
   101               buffer.remove(caret - len, len)
   102               buffer.insert(caret - len, item.replacement)
   103             case _ =>
   104           }
   105         }
   106       }
   107     }
   108 
   109 
   110     /* input of key events */
   111 
   112     def input(evt: KeyEvent)
   113     {
   114       Swing_Thread.require()
   115 
   116       if (PIDE.options.bool("jedit_completion")) {
   117         if (!evt.isConsumed) {
   118           dismissed()
   119           input_delay.invoke()
   120         }
   121       }
   122       else {
   123         dismissed()
   124         input_delay.revoke()
   125       }
   126     }
   127 
   128     private val input_delay =
   129       Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay"))
   130       {
   131         val view = text_area.getView
   132         val layered = view.getLayeredPane
   133         val buffer = text_area.getBuffer
   134         val painter = text_area.getPainter
   135 
   136         if (buffer.isEditable) {
   137           Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
   138             case Some(syntax) =>
   139               val caret = text_area.getCaretPosition
   140               val line = buffer.getLineOfOffset(caret)
   141               val start = buffer.getLineStartOffset(line)
   142               val text = buffer.getSegment(start, caret - start)
   143 
   144               syntax.completion.complete(Isabelle_Encoding.is_active(buffer), text) match {
   145                 case Some((original, items)) =>
   146                   val font =
   147                     painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
   148 
   149                   val loc1 = text_area.offsetToXY(caret - original.length)
   150                   if (loc1 != null) {
   151                     val loc2 =
   152                       SwingUtilities.convertPoint(painter,
   153                         loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
   154 
   155                     val completion =
   156                       new Completion_Popup(layered, loc2, font, items) {
   157                         override def complete(item: Completion.Item) { insert(item) }
   158                         override def propagate(evt: KeyEvent) {
   159                           JEdit_Lib.propagate_key(view, evt)
   160                           input(evt)
   161                         }
   162                         override def refocus() { text_area.requestFocus }
   163                       }
   164                     completion_popup = Some(completion)
   165                     completion.show_popup()
   166                   }
   167                 case None =>
   168               }
   169             case None =>
   170           }
   171         }
   172       }
   173 
   174 
   175     /* activation */
   176 
   177     private val outer_key_listener =
   178       JEdit_Lib.key_listener(key_typed = input _)
   179 
   180     private def activate()
   181     {
   182       text_area.addKeyListener(outer_key_listener)
   183     }
   184 
   185     private def deactivate()
   186     {
   187       dismissed()
   188       text_area.removeKeyListener(outer_key_listener)
   189     }
   190   }
   191 }
   192 
   193 
   194 class Completion_Popup private(
   195   layered: JLayeredPane,
   196   location: Point,
   197   font: Font,
   198   items: List[Completion.Item]) extends JPanel(new BorderLayout)
   199 {
   200   completion =>
   201 
   202   Swing_Thread.require()
   203   require(!items.isEmpty)
   204 
   205 
   206   /* actions */
   207 
   208   def complete(item: Completion.Item) { }
   209   def propagate(evt: KeyEvent) { }
   210   def refocus() { }
   211 
   212 
   213   /* list view */
   214 
   215   private val list_view = new ListView(items)
   216   list_view.font = font
   217   list_view.selection.intervalMode = ListView.IntervalMode.Single
   218   list_view.peer.setFocusTraversalKeysEnabled(false)
   219   list_view.peer.setVisibleRowCount(items.length min 8)
   220   list_view.peer.setSelectedIndex(0)
   221 
   222   private def complete_selected(): Boolean =
   223   {
   224     list_view.selection.items.toList match {
   225       case item :: _ => complete(item); true
   226       case _ => false
   227     }
   228   }
   229 
   230   private def move_items(n: Int)
   231   {
   232     val i = list_view.peer.getSelectedIndex
   233     val j = ((i + n) min (items.length - 1)) max 0
   234     if (i != j) {
   235       list_view.peer.setSelectedIndex(j)
   236       list_view.peer.ensureIndexIsVisible(j)
   237     }
   238   }
   239 
   240   private def move_pages(n: Int)
   241   {
   242     val page_size = list_view.peer.getVisibleRowCount - 1
   243     move_items(page_size * n)
   244   }
   245 
   246 
   247   /* event handling */
   248 
   249   private val inner_key_listener =
   250     JEdit_Lib.key_listener(
   251       key_pressed = (e: KeyEvent) =>
   252         {
   253           if (!e.isConsumed) {
   254             e.getKeyCode match {
   255               case KeyEvent.VK_TAB =>
   256                 if (complete_selected()) e.consume
   257                 hide_popup()
   258               case KeyEvent.VK_ESCAPE =>
   259                 hide_popup()
   260                 e.consume
   261               case KeyEvent.VK_UP => move_items(-1); e.consume
   262               case KeyEvent.VK_DOWN => move_items(1); e.consume
   263               case KeyEvent.VK_PAGE_UP => move_pages(-1); e.consume
   264               case KeyEvent.VK_PAGE_DOWN => move_pages(1); e.consume
   265               case _ =>
   266                 if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown)
   267                   hide_popup()
   268             }
   269           }
   270           propagate(e)
   271         },
   272       key_typed = propagate _
   273     )
   274 
   275   list_view.peer.addKeyListener(inner_key_listener)
   276 
   277   list_view.peer.addMouseListener(new MouseAdapter {
   278     override def mouseClicked(e: MouseEvent) {
   279       if (complete_selected()) e.consume
   280       hide_popup()
   281     }
   282   })
   283 
   284   list_view.peer.addFocusListener(new FocusAdapter {
   285     override def focusLost(e: FocusEvent) { hide_popup() }
   286   })
   287 
   288 
   289   /* main content */
   290 
   291   override def getFocusTraversalKeysEnabled = false
   292 
   293   completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent])
   294 
   295 
   296   /* popup */
   297 
   298   private val popup =
   299   {
   300     val screen = JEdit_Lib.screen_location(layered, location)
   301     val size =
   302     {
   303       val geometry = JEdit_Lib.window_geometry(completion, completion)
   304       val bounds = Rendering.popup_bounds
   305       val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth
   306       val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight
   307       new Dimension(w, h)
   308     }
   309     new Popup(layered, completion, screen.relative(layered, size), size)
   310   }
   311 
   312   private def show_popup()
   313   {
   314     popup.show
   315     list_view.requestFocus
   316   }
   317 
   318   private def hide_popup()
   319   {
   320     val had_focus = list_view.peer.isFocusOwner
   321     popup.hide
   322     if (had_focus) refocus()
   323   }
   324 }
   325