src/Tools/jEdit/src/completion_popup.scala
author wenzelm
Mon Feb 24 12:23:35 2014 +0100 (2014-02-24 ago)
changeset 55712 e757e8c8d8ea
parent 55711 9e3d64e5919a
child 55747 bef19c929ba5
permissions -rw-r--r--
tuned signature -- weaker type requirement;
     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.{Color, Font, Point, BorderLayout, Dimension}
    13 import java.awt.event.{KeyEvent, MouseEvent, MouseAdapter, FocusAdapter, FocusEvent}
    14 import javax.swing.{JPanel, JComponent, JLayeredPane, SwingUtilities}
    15 import javax.swing.border.LineBorder
    16 import javax.swing.text.DefaultCaret
    17 
    18 import scala.swing.{ListView, ScrollPane}
    19 import scala.swing.event.MouseClicked
    20 
    21 import org.gjt.sp.jedit.View
    22 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
    23 import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
    24 
    25 
    26 object Completion_Popup
    27 {
    28   /** jEdit text area **/
    29 
    30   object Text_Area
    31   {
    32     private val key = new Object
    33 
    34     def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
    35     {
    36       Swing_Thread.require()
    37       text_area.getClientProperty(key) match {
    38         case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
    39         case _ => None
    40       }
    41     }
    42 
    43     def active_range(text_area: TextArea): Option[Text.Range] =
    44       apply(text_area) match {
    45         case Some(text_area_completion) => text_area_completion.active_range
    46         case None => None
    47       }
    48 
    49     def exit(text_area: JEditTextArea)
    50     {
    51       Swing_Thread.require()
    52       apply(text_area) match {
    53         case None =>
    54         case Some(text_area_completion) =>
    55           text_area_completion.deactivate()
    56           text_area.putClientProperty(key, null)
    57       }
    58     }
    59 
    60     def init(text_area: JEditTextArea): Completion_Popup.Text_Area =
    61     {
    62       exit(text_area)
    63       val text_area_completion = new Text_Area(text_area)
    64       text_area.putClientProperty(key, text_area_completion)
    65       text_area_completion.activate()
    66       text_area_completion
    67     }
    68 
    69     def dismissed(text_area: TextArea): Boolean =
    70     {
    71       Swing_Thread.require()
    72       apply(text_area) match {
    73         case Some(text_area_completion) => text_area_completion.dismissed()
    74         case None => false
    75       }
    76     }
    77   }
    78 
    79   class Text_Area private(text_area: JEditTextArea)
    80   {
    81     // owned by Swing thread
    82     private var completion_popup: Option[Completion_Popup] = None
    83 
    84     def active_range: Option[Text.Range] =
    85       completion_popup match {
    86         case Some(completion) =>
    87           completion.active_range match {
    88             case Some((range, _)) if completion.isDisplayable => Some(range)
    89             case _ => None
    90           }
    91         case None => None
    92       }
    93 
    94 
    95     /* completion action */
    96 
    97     private def insert(item: Completion.Item)
    98     {
    99       Swing_Thread.require()
   100 
   101       val buffer = text_area.getBuffer
   102       val range = item.range
   103       if (buffer.isEditable && range.length > 0) {
   104         JEdit_Lib.buffer_edit(buffer) {
   105           JEdit_Lib.try_get_text(buffer, range) match {
   106             case Some(text) if text == item.original =>
   107               buffer.remove(range.start, range.length)
   108               buffer.insert(range.start, item.replacement)
   109               text_area.moveCaretPosition(range.start + item.replacement.length + item.move)
   110             case _ =>
   111           }
   112         }
   113       }
   114     }
   115 
   116     def action(immediate: Boolean = false, explicit: Boolean = false)
   117     {
   118       val view = text_area.getView
   119       val layered = view.getLayeredPane
   120       val buffer = text_area.getBuffer
   121       val painter = text_area.getPainter
   122       val caret = text_area.getCaretPosition
   123 
   124       val history = PIDE.completion_history.value
   125       val decode = Isabelle_Encoding.is_active(buffer)
   126 
   127       def open_popup(result: Completion.Result)
   128       {
   129         val font =
   130           painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
   131 
   132         val range = result.range
   133         def invalidate(): Unit = JEdit_Lib.invalidate_range(text_area, range)
   134 
   135         val loc1 = text_area.offsetToXY(range.start)
   136         if (loc1 != null) {
   137           val loc2 =
   138             SwingUtilities.convertPoint(painter,
   139               loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
   140 
   141           val completion =
   142             new Completion_Popup(Some((range, invalidate _)), layered, loc2, font, result.items) {
   143               override def complete(item: Completion.Item) {
   144                 PIDE.completion_history.update(item)
   145                 insert(item)
   146               }
   147               override def propagate(evt: KeyEvent) {
   148                 JEdit_Lib.propagate_key(view, evt)
   149                 input(evt)
   150               }
   151               override def refocus() { text_area.requestFocus }
   152             }
   153           completion_popup = Some(completion)
   154           invalidate()
   155           completion.show_popup()
   156         }
   157       }
   158 
   159       def semantic_completion(): Boolean =
   160         explicit && {
   161           PIDE.document_view(text_area) match {
   162             case Some(doc_view) =>
   163               val rendering = doc_view.get_rendering()
   164               rendering.completion_names(JEdit_Lib.stretch_point_range(buffer, caret)) match {
   165                 case None => false
   166                 case Some(names) =>
   167                   JEdit_Lib.try_get_text(buffer, names.range) match {
   168                     case Some(original) =>
   169                       names.complete(history, decode, original) match {
   170                         case Some(result) if !result.items.isEmpty =>
   171                           open_popup(result)
   172                           true
   173                         case _ => false
   174                       }
   175                     case None => false
   176                   }
   177               }
   178             case _ => false
   179           }
   180         }
   181 
   182       def syntax_completion(): Boolean =
   183       {
   184         Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
   185           case Some(syntax) =>
   186             val line = buffer.getLineOfOffset(caret)
   187             val start = buffer.getLineStartOffset(line)
   188             val text = buffer.getSegment(start, caret - start)
   189 
   190             val context =
   191               (PIDE.document_view(text_area) match {
   192                 case None => None
   193                 case Some(doc_view) =>
   194                   val rendering = doc_view.get_rendering()
   195                   rendering.completion_context(JEdit_Lib.stretch_point_range(buffer, caret))
   196               }) getOrElse syntax.completion_context
   197 
   198             syntax.completion.complete(history, decode, explicit, start, text, context) match {
   199               case Some(result) =>
   200                 result.items match {
   201                   case List(item) if result.unique && item.immediate && immediate =>
   202                     insert(item)
   203                     true
   204                   case _ :: _ =>
   205                     open_popup(result)
   206                     true
   207                   case _ => false
   208                 }
   209               case None => false
   210             }
   211           case None => false
   212         }
   213       }
   214 
   215       if (buffer.isEditable)
   216         semantic_completion() || syntax_completion()
   217     }
   218 
   219 
   220     /* input key events */
   221 
   222     def input(evt: KeyEvent)
   223     {
   224       Swing_Thread.require()
   225 
   226       if (PIDE.options.bool("jedit_completion")) {
   227         if (!evt.isConsumed) {
   228           dismissed()
   229           if (evt.getKeyChar != '\b') {
   230             val special = JEdit_Lib.special_key(evt)
   231             if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
   232               input_delay.revoke()
   233               action(immediate = PIDE.options.bool("jedit_completion_immediate"))
   234             }
   235             else input_delay.invoke()
   236           }
   237         }
   238       }
   239     }
   240 
   241     private val input_delay =
   242       Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
   243         action()
   244       }
   245 
   246 
   247     /* dismiss popup */
   248 
   249     def dismissed(): Boolean =
   250     {
   251       Swing_Thread.require()
   252 
   253       completion_popup match {
   254         case Some(completion) =>
   255           completion.hide_popup()
   256           completion_popup = None
   257           true
   258         case None =>
   259           false
   260       }
   261     }
   262 
   263 
   264     /* activation */
   265 
   266     private val outer_key_listener =
   267       JEdit_Lib.key_listener(key_typed = input _)
   268 
   269     private def activate()
   270     {
   271       text_area.addKeyListener(outer_key_listener)
   272     }
   273 
   274     private def deactivate()
   275     {
   276       dismissed()
   277       text_area.removeKeyListener(outer_key_listener)
   278     }
   279   }
   280 
   281 
   282 
   283   /** history text field **/
   284 
   285   class History_Text_Field(
   286     name: String = null,
   287     instant_popups: Boolean = false,
   288     enter_adds_to_history: Boolean = true,
   289     syntax: Outer_Syntax = Outer_Syntax.init) extends
   290     HistoryTextField(name, instant_popups, enter_adds_to_history)
   291   {
   292     text_field =>
   293 
   294     // see https://forums.oracle.com/thread/1361677
   295     if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret)
   296 
   297     // owned by Swing thread
   298     private var completion_popup: Option[Completion_Popup] = None
   299 
   300 
   301     /* dismiss */
   302 
   303     private def dismissed(): Boolean =
   304     {
   305       completion_popup match {
   306         case Some(completion) =>
   307           completion.hide_popup()
   308           completion_popup = None
   309           true
   310         case None =>
   311           false
   312       }
   313     }
   314 
   315 
   316     /* insert */
   317 
   318     private def insert(item: Completion.Item)
   319     {
   320       Swing_Thread.require()
   321 
   322       val range = item.range
   323       if (text_field.isEditable && range.length > 0) {
   324         val content = text_field.getText
   325         JEdit_Lib.try_get_text(content, range) match {
   326           case Some(text) if text == item.original =>
   327             text_field.setText(
   328               content.substring(0, range.start) +
   329               item.replacement +
   330               content.substring(range.stop))
   331             text_field.getCaret.setDot(range.start + item.replacement.length + item.move)
   332           case _ =>
   333         }
   334       }
   335     }
   336 
   337 
   338     /* completion action */
   339 
   340     def action()
   341     {
   342       GUI.layered_pane(text_field) match {
   343         case Some(layered) if text_field.isEditable =>
   344           val history = PIDE.completion_history.value
   345 
   346           val caret = text_field.getCaret.getDot
   347           val text = text_field.getText.substring(0, caret)
   348 
   349           syntax.completion.complete(
   350               history, decode = true, explicit = false, 0, text, syntax.completion_context) match {
   351             case Some(result) =>
   352               val fm = text_field.getFontMetrics(text_field.getFont)
   353               val loc =
   354                 SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
   355 
   356               val completion =
   357                 new Completion_Popup(None, layered, loc, text_field.getFont, result.items)
   358               {
   359                 override def complete(item: Completion.Item) {
   360                   PIDE.completion_history.update(item)
   361                   insert(item)
   362                 }
   363                 override def propagate(evt: KeyEvent) {
   364                   if (!evt.isConsumed) text_field.processKeyEvent(evt)
   365                 }
   366                 override def refocus() { text_field.requestFocus }
   367               }
   368               completion_popup = Some(completion)
   369               completion.show_popup()
   370 
   371             case None =>
   372           }
   373         case _ =>
   374       }
   375     }
   376 
   377 
   378     /* process key event */
   379 
   380     private def process(evt: KeyEvent)
   381     {
   382       if (PIDE.options.bool("jedit_completion")) {
   383         dismissed()
   384         if (evt.getKeyChar != '\b') {
   385           val special = JEdit_Lib.special_key(evt)
   386           if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
   387             process_delay.revoke()
   388             action()
   389           }
   390           else process_delay.invoke()
   391         }
   392       }
   393     }
   394 
   395     private val process_delay =
   396       Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
   397         action()
   398       }
   399 
   400     override def processKeyEvent(evt0: KeyEvent)
   401     {
   402       val evt = KeyEventWorkaround.processKeyEvent(evt0)
   403       if (evt != null) {
   404         evt.getID match {
   405           case KeyEvent.KEY_PRESSED =>
   406             val key_code = evt.getKeyCode
   407             if (key_code == KeyEvent.VK_ESCAPE) {
   408               if (dismissed()) evt.consume
   409             }
   410           case KeyEvent.KEY_TYPED =>
   411             super.processKeyEvent(evt)
   412             process(evt)
   413             evt.consume
   414           case _ =>
   415         }
   416         if (!evt.isConsumed) super.processKeyEvent(evt)
   417       }
   418     }
   419   }
   420 }
   421 
   422 
   423 class Completion_Popup private(
   424   val active_range: Option[(Text.Range, () => Unit)],
   425   layered: JLayeredPane,
   426   location: Point,
   427   font: Font,
   428   items: List[Completion.Item]) extends JPanel(new BorderLayout)
   429 {
   430   completion =>
   431 
   432   Swing_Thread.require()
   433 
   434   require(!items.isEmpty)
   435   val multi = items.length > 1
   436 
   437 
   438   /* actions */
   439 
   440   def complete(item: Completion.Item) { }
   441   def propagate(evt: KeyEvent) { }
   442   def refocus() { }
   443 
   444 
   445   /* list view */
   446 
   447   private val list_view = new ListView(items)
   448   list_view.font = font
   449   list_view.selection.intervalMode = ListView.IntervalMode.Single
   450   list_view.peer.setFocusTraversalKeysEnabled(false)
   451   list_view.peer.setVisibleRowCount(items.length min 8)
   452   list_view.peer.setSelectedIndex(0)
   453 
   454   for (cond <-
   455     List(JComponent.WHEN_FOCUSED,
   456       JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT,
   457       JComponent.WHEN_IN_FOCUSED_WINDOW)) list_view.peer.setInputMap(cond, null)
   458 
   459   private def complete_selected(): Boolean =
   460   {
   461     list_view.selection.items.toList match {
   462       case item :: _ => complete(item); true
   463       case _ => false
   464     }
   465   }
   466 
   467   private def move_items(n: Int)
   468   {
   469     val i = list_view.peer.getSelectedIndex
   470     val j = ((i + n) min (items.length - 1)) max 0
   471     if (i != j) {
   472       list_view.peer.setSelectedIndex(j)
   473       list_view.peer.ensureIndexIsVisible(j)
   474     }
   475   }
   476 
   477   private def move_pages(n: Int)
   478   {
   479     val page_size = list_view.peer.getVisibleRowCount - 1
   480     move_items(page_size * n)
   481   }
   482 
   483 
   484   /* event handling */
   485 
   486   private val inner_key_listener =
   487     JEdit_Lib.key_listener(
   488       key_pressed = (e: KeyEvent) =>
   489         {
   490           if (!e.isConsumed) {
   491             e.getKeyCode match {
   492               case KeyEvent.VK_TAB =>
   493                 if (complete_selected()) e.consume
   494                 hide_popup()
   495               case KeyEvent.VK_ESCAPE =>
   496                 hide_popup()
   497                 e.consume
   498               case KeyEvent.VK_UP | KeyEvent.VK_KP_UP if multi =>
   499                 move_items(-1)
   500                 e.consume
   501               case KeyEvent.VK_DOWN | KeyEvent.VK_KP_DOWN if multi =>
   502                 move_items(1)
   503                 e.consume
   504               case KeyEvent.VK_PAGE_UP if multi =>
   505                 move_pages(-1)
   506                 e.consume
   507               case KeyEvent.VK_PAGE_DOWN if multi =>
   508                 move_pages(1)
   509                 e.consume
   510               case _ =>
   511                 if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown)
   512                   hide_popup()
   513             }
   514           }
   515           propagate(e)
   516         },
   517       key_typed = propagate _
   518     )
   519 
   520   list_view.peer.addKeyListener(inner_key_listener)
   521 
   522   list_view.peer.addMouseListener(new MouseAdapter {
   523     override def mouseClicked(e: MouseEvent) {
   524       if (complete_selected()) e.consume
   525       hide_popup()
   526     }
   527   })
   528 
   529   list_view.peer.addFocusListener(new FocusAdapter {
   530     override def focusLost(e: FocusEvent) { hide_popup() }
   531   })
   532 
   533 
   534   /* main content */
   535 
   536   override def getFocusTraversalKeysEnabled = false
   537   completion.setBorder(new LineBorder(Color.BLACK))
   538   completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent])
   539 
   540 
   541   /* popup */
   542 
   543   private val popup =
   544   {
   545     val screen = JEdit_Lib.screen_location(layered, location)
   546     val size =
   547     {
   548       val geometry = JEdit_Lib.window_geometry(completion, completion)
   549       val bounds = Rendering.popup_bounds
   550       val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth
   551       val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight
   552       new Dimension(w, h)
   553     }
   554     new Popup(layered, completion, screen.relative(layered, size), size)
   555   }
   556 
   557   private def show_popup()
   558   {
   559     popup.show
   560     list_view.requestFocus
   561   }
   562 
   563   private val hide_popup_delay =
   564     Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_dismiss_delay")) {
   565       active_range match { case Some((_, invalidate)) => invalidate() case _ => }
   566       popup.hide
   567     }
   568 
   569   private def hide_popup()
   570   {
   571     if (list_view.peer.isFocusOwner) refocus()
   572 
   573     if (PIDE.options.seconds("jedit_completion_dismiss_delay").is_zero) {
   574       active_range match { case Some((_, invalidate)) => invalidate() case _ => }
   575       popup.hide
   576     }
   577     else hide_popup_delay.invoke()
   578   }
   579 }
   580