src/Tools/jEdit/src/completion_popup.scala
author wenzelm
Sat May 03 20:31:29 2014 +0200 (2014-05-03 ago)
changeset 56842 b6e266574b26
parent 56841 bc6faeadbf82
child 56843 b2bfcd8cda80
permissions -rw-r--r--
yet another completion option, to imitate old less ambitious behavior;
     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, Selection}
    23 import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
    24 
    25 
    26 object Completion_Popup
    27 {
    28   /** items with HTML rendering **/
    29 
    30   private class Item(val item: Completion.Item)
    31   {
    32     private val html =
    33       item.description match {
    34         case a :: bs =>
    35           "<html><b>" + HTML.encode(a) + "</b>" +
    36             HTML.encode(bs.map(" " + _).mkString) + "</html>"
    37         case Nil => ""
    38       }
    39     override def toString: String = html
    40   }
    41 
    42 
    43 
    44   /** jEdit text area **/
    45 
    46   object Text_Area
    47   {
    48     private val key = new Object
    49 
    50     def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
    51     {
    52       Swing_Thread.require {}
    53       text_area.getClientProperty(key) match {
    54         case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
    55         case _ => None
    56       }
    57     }
    58 
    59     def active_range(text_area: TextArea): Option[Text.Range] =
    60       apply(text_area) match {
    61         case Some(text_area_completion) => text_area_completion.active_range
    62         case None => None
    63       }
    64 
    65     def action(text_area: TextArea, word_only: Boolean): Boolean =
    66       apply(text_area) match {
    67         case Some(text_area_completion) =>
    68           if (text_area_completion.active_range.isDefined)
    69             text_area_completion.action(word_only = word_only)
    70           else
    71             text_area_completion.action(immediate = true, explicit = true, word_only = word_only)
    72           true
    73         case None => false
    74       }
    75 
    76     def exit(text_area: JEditTextArea)
    77     {
    78       Swing_Thread.require {}
    79       apply(text_area) match {
    80         case None =>
    81         case Some(text_area_completion) =>
    82           text_area_completion.deactivate()
    83           text_area.putClientProperty(key, null)
    84       }
    85     }
    86 
    87     def init(text_area: JEditTextArea): Completion_Popup.Text_Area =
    88     {
    89       exit(text_area)
    90       val text_area_completion = new Text_Area(text_area)
    91       text_area.putClientProperty(key, text_area_completion)
    92       text_area_completion.activate()
    93       text_area_completion
    94     }
    95 
    96     def dismissed(text_area: TextArea): Boolean =
    97     {
    98       Swing_Thread.require {}
    99       apply(text_area) match {
   100         case Some(text_area_completion) => text_area_completion.dismissed()
   101         case None => false
   102       }
   103     }
   104   }
   105 
   106   class Text_Area private(text_area: JEditTextArea)
   107   {
   108     // owned by Swing thread
   109     private var completion_popup: Option[Completion_Popup] = None
   110 
   111     def active_range: Option[Text.Range] =
   112       completion_popup match {
   113         case Some(completion) => completion.active_range
   114         case None => None
   115       }
   116 
   117 
   118     /* rendering */
   119 
   120     def rendering(rendering: Rendering, line_range: Text.Range): Option[Text.Info[Color]] =
   121     {
   122       active_range match {
   123         case Some(range) => range.try_restrict(line_range)
   124         case None =>
   125           if (line_range.contains(text_area.getCaretPosition)) {
   126             JEdit_Lib.before_caret_range(text_area, rendering).try_restrict(line_range) match {
   127               case Some(range) if !range.is_singularity =>
   128                 rendering.semantic_completion(range) match {
   129                   case Some(Text.Info(_, Completion.No_Completion)) => None
   130                   case Some(Text.Info(range1, _: Completion.Names)) => Some(range1)
   131                   case None =>
   132                     syntax_completion(Completion.History.empty, false, Some(rendering)).map(_.range)
   133                 }
   134               case _ => None
   135             }
   136           }
   137           else None
   138       }
   139     }.map(range => Text.Info(range, rendering.completion_color))
   140 
   141 
   142     /* syntax completion */
   143 
   144     def syntax_completion(
   145       history: Completion.History,
   146       explicit: Boolean,
   147       opt_rendering: Option[Rendering]): Option[Completion.Result] =
   148     {
   149       val buffer = text_area.getBuffer
   150       val decode = Isabelle_Encoding.is_active(buffer)
   151 
   152       Isabelle.mode_syntax(JEdit_Lib.buffer_mode(buffer)) match {
   153         case Some(syntax) =>
   154           val context =
   155             (for {
   156               rendering <- opt_rendering
   157               if PIDE.options.bool("jedit_completion_context")
   158               range = JEdit_Lib.before_caret_range(text_area, rendering)
   159               context <- rendering.language_context(range)
   160             } yield context) getOrElse syntax.language_context
   161 
   162           val caret = text_area.getCaretPosition
   163           val line_range = JEdit_Lib.line_range(buffer, text_area.getCaretLine)
   164           val line_start = line_range.start
   165           for {
   166             line_text <- JEdit_Lib.try_get_text(buffer, line_range)
   167             result <-
   168               syntax.completion.complete(
   169                 history, decode, explicit, line_start, line_text, caret - line_start, false, context)
   170           } yield result
   171 
   172         case None => None
   173       }
   174     }
   175 
   176 
   177     /* spell-checker completion */
   178 
   179     def spell_checker_completion(rendering: Rendering): Option[Completion.Result] =
   180     {
   181       for {
   182         spell_checker <- PIDE.spell_checker.get
   183         range = JEdit_Lib.before_caret_range(text_area, rendering)
   184         word <- Spell_Checker.current_word(text_area, rendering, range)
   185         words = spell_checker.complete(word.info)
   186         if !words.isEmpty
   187         descr = "(from dictionary " + quote(spell_checker.toString) + ")"
   188         items =
   189           words.map(w => Completion.Item(word.range, word.info, "", List(w, descr), w, 0, false))
   190       } yield Completion.Result(word.range, word.info, false, items)
   191     }
   192 
   193 
   194     /* completion action: text area */
   195 
   196     private def insert(item: Completion.Item)
   197     {
   198       Swing_Thread.require {}
   199 
   200       val buffer = text_area.getBuffer
   201       val range = item.range
   202       if (buffer.isEditable && range.length > 0) {
   203         JEdit_Lib.buffer_edit(buffer) {
   204           JEdit_Lib.try_get_text(buffer, range) match {
   205             case Some(text) if text == item.original =>
   206               text_area.getSelectionAtOffset(text_area.getCaretPosition) match {
   207 
   208                 /*rectangular selection as "tall caret"*/
   209                 case selection : Selection.Rect
   210                 if selection.getStart(buffer, text_area.getCaretLine) == range.stop =>
   211                   text_area.moveCaretPosition(range.stop)
   212                   (0 until Character.codePointCount(item.original, 0, item.original.length))
   213                     .foreach(_ => text_area.backspace())
   214                   text_area.setSelectedText(selection, item.replacement)
   215                   text_area.moveCaretPosition(text_area.getCaretPosition + item.move)
   216 
   217                 /*other selections: rectangular, multiple range, ...*/
   218                 case selection
   219                 if selection != null &&
   220                     selection.getStart(buffer, text_area.getCaretLine) == range.start &&
   221                     selection.getEnd(buffer, text_area.getCaretLine) == range.stop =>
   222                   text_area.moveCaretPosition(range.stop + item.move)
   223                   text_area.getSelection.foreach(text_area.setSelectedText(_, item.replacement))
   224 
   225                 /*no selection*/
   226                 case _ =>
   227                   buffer.remove(range.start, range.length)
   228                   buffer.insert(range.start, item.replacement)
   229                   text_area.moveCaretPosition(range.start + item.replacement.length + item.move)
   230               }
   231             case _ =>
   232           }
   233         }
   234       }
   235     }
   236 
   237     def action(
   238       immediate: Boolean = false,
   239       explicit: Boolean = false,
   240       delayed: Boolean = false,
   241       word_only: Boolean = false): Boolean =
   242     {
   243       val view = text_area.getView
   244       val layered = view.getLayeredPane
   245       val buffer = text_area.getBuffer
   246       val painter = text_area.getPainter
   247 
   248       val history = PIDE.completion_history.value
   249       val decode = Isabelle_Encoding.is_active(buffer)
   250 
   251       def open_popup(result: Completion.Result)
   252       {
   253         val font =
   254           painter.getFont.deriveFont(
   255             Font_Info.main_size(PIDE.options.real("jedit_popup_font_scale")))
   256 
   257         val range = result.range
   258 
   259         val loc1 = text_area.offsetToXY(range.start)
   260         if (loc1 != null) {
   261           val loc2 =
   262             SwingUtilities.convertPoint(painter,
   263               loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
   264 
   265           val items = result.items.map(new Item(_))
   266           val completion =
   267             new Completion_Popup(Some(range), layered, loc2, font, items)
   268             {
   269               override def complete(item: Completion.Item) {
   270                 PIDE.completion_history.update(item)
   271                 insert(item)
   272               }
   273               override def propagate(evt: KeyEvent) {
   274                 if (view.getKeyEventInterceptor == null)
   275                   JEdit_Lib.propagate_key(view, evt)
   276                 else if (view.getKeyEventInterceptor == inner_key_listener) {
   277                   try {
   278                     view.setKeyEventInterceptor(null)
   279                     JEdit_Lib.propagate_key(view, evt)
   280                   }
   281                   finally {
   282                     if (isDisplayable) view.setKeyEventInterceptor(inner_key_listener)
   283                   }
   284                 }
   285                 if (evt.getID == KeyEvent.KEY_TYPED) input(evt)
   286               }
   287               override def shutdown(focus: Boolean) {
   288                 if (view.getKeyEventInterceptor == inner_key_listener)
   289                   view.setKeyEventInterceptor(null)
   290                 if (focus) text_area.requestFocus
   291                 JEdit_Lib.invalidate_range(text_area, range)
   292               }
   293             }
   294           completion_popup = Some(completion)
   295           view.setKeyEventInterceptor(completion.inner_key_listener)
   296           JEdit_Lib.invalidate_range(text_area, range)
   297           Pretty_Tooltip.dismissed_all()
   298           completion.show_popup(false)
   299         }
   300       }
   301 
   302       if (buffer.isEditable) {
   303         val (no_completion, semantic_completion, opt_rendering) =
   304         {
   305           PIDE.document_view(text_area) match {
   306             case Some(doc_view) =>
   307               val rendering = doc_view.get_rendering()
   308               val (no_completion, result) =
   309               {
   310                 val caret_range = JEdit_Lib.before_caret_range(text_area, rendering)
   311                 rendering.semantic_completion(caret_range) match {
   312                   case Some(Text.Info(_, Completion.No_Completion)) => (true, None)
   313                   case Some(Text.Info(range, names: Completion.Names)) =>
   314                     val result =
   315                       JEdit_Lib.try_get_text(buffer, range) match {
   316                         case Some(original) => names.complete(range, history, decode, original)
   317                         case None => None
   318                       }
   319                     (false, result)
   320                   case None => (false, None)
   321                 }
   322               }
   323               (no_completion, result, Some(rendering))
   324             case None => (false, None, None)
   325           }
   326         }
   327         if (no_completion) false
   328         else {
   329           val result =
   330           {
   331             val result0 =
   332               if (word_only) None
   333               else
   334                 Completion.Result.merge(history, semantic_completion,
   335                   syntax_completion(history, explicit, opt_rendering))
   336             opt_rendering match {
   337               case None => result0
   338               case Some(rendering) =>
   339                 Completion.Result.merge(history, result0, spell_checker_completion(rendering))
   340             }
   341           }
   342           result match {
   343             case Some(result) =>
   344               result.items match {
   345                 case List(item) if result.unique && item.immediate && immediate =>
   346                   insert(item)
   347                   true
   348                 case _ :: _ if !delayed =>
   349                   open_popup(result)
   350                   false
   351                 case _ => false
   352               }
   353             case None => false
   354           }
   355         }
   356       }
   357       else false
   358     }
   359 
   360 
   361     /* input key events */
   362 
   363     def input(evt: KeyEvent)
   364     {
   365       Swing_Thread.require {}
   366 
   367       if (PIDE.options.bool("jedit_completion")) {
   368         if (!evt.isConsumed) {
   369           dismissed()
   370           if (evt.getKeyChar != '\b') {
   371             val special = JEdit_Lib.special_key(evt)
   372             val immediate = PIDE.options.bool("jedit_completion_immediate")
   373             if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
   374               input_delay.revoke()
   375               action(immediate = immediate)
   376             }
   377             else {
   378               if (!special && action(immediate = immediate, delayed = true))
   379                 input_delay.revoke()
   380               else
   381                 input_delay.invoke()
   382             }
   383           }
   384         }
   385       }
   386     }
   387 
   388     private val input_delay =
   389       Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
   390         action()
   391       }
   392 
   393 
   394     /* dismiss popup */
   395 
   396     def dismissed(): Boolean =
   397     {
   398       Swing_Thread.require {}
   399 
   400       completion_popup match {
   401         case Some(completion) =>
   402           completion.hide_popup()
   403           completion_popup = None
   404           true
   405         case None =>
   406           false
   407       }
   408     }
   409 
   410 
   411     /* activation */
   412 
   413     private val outer_key_listener =
   414       JEdit_Lib.key_listener(key_typed = input _)
   415 
   416     private def activate()
   417     {
   418       text_area.addKeyListener(outer_key_listener)
   419     }
   420 
   421     private def deactivate()
   422     {
   423       dismissed()
   424       text_area.removeKeyListener(outer_key_listener)
   425     }
   426   }
   427 
   428 
   429 
   430   /** history text field **/
   431 
   432   class History_Text_Field(
   433     name: String = null,
   434     instant_popups: Boolean = false,
   435     enter_adds_to_history: Boolean = true,
   436     syntax: Outer_Syntax = Outer_Syntax.init) extends
   437     HistoryTextField(name, instant_popups, enter_adds_to_history)
   438   {
   439     text_field =>
   440 
   441     // see https://forums.oracle.com/thread/1361677
   442     if (GUI.is_macos_laf) text_field.setCaret(new DefaultCaret)
   443 
   444     // owned by Swing thread
   445     private var completion_popup: Option[Completion_Popup] = None
   446 
   447 
   448     /* dismiss */
   449 
   450     private def dismissed(): Boolean =
   451     {
   452       completion_popup match {
   453         case Some(completion) =>
   454           completion.hide_popup()
   455           completion_popup = None
   456           true
   457         case None =>
   458           false
   459       }
   460     }
   461 
   462 
   463     /* insert */
   464 
   465     private def insert(item: Completion.Item)
   466     {
   467       Swing_Thread.require {}
   468 
   469       val range = item.range
   470       if (text_field.isEditable && range.length > 0) {
   471         val content = text_field.getText
   472         JEdit_Lib.try_get_text(content, range) match {
   473           case Some(text) if text == item.original =>
   474             text_field.setText(
   475               content.substring(0, range.start) +
   476               item.replacement +
   477               content.substring(range.stop))
   478             text_field.getCaret.setDot(range.start + item.replacement.length + item.move)
   479           case _ =>
   480         }
   481       }
   482     }
   483 
   484 
   485     /* completion action: text field */
   486 
   487     def action()
   488     {
   489       GUI.layered_pane(text_field) match {
   490         case Some(layered) if text_field.isEditable =>
   491           val history = PIDE.completion_history.value
   492 
   493           val caret = text_field.getCaret.getDot
   494           val text = text_field.getText
   495 
   496           val context = syntax.language_context
   497 
   498           syntax.completion.complete(history, true, false, 0, text, caret, false, context) match {
   499             case Some(result) =>
   500               val fm = text_field.getFontMetrics(text_field.getFont)
   501               val loc =
   502                 SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
   503 
   504               val items = result.items.map(new Item(_))
   505               val completion =
   506                 new Completion_Popup(None, layered, loc, text_field.getFont, items)
   507                 {
   508                   override def complete(item: Completion.Item) {
   509                     PIDE.completion_history.update(item)
   510                     insert(item)
   511                   }
   512                   override def propagate(evt: KeyEvent) {
   513                     if (!evt.isConsumed) text_field.processKeyEvent(evt)
   514                   }
   515                   override def shutdown(focus: Boolean) { if (focus) text_field.requestFocus }
   516                 }
   517               completion_popup = Some(completion)
   518               completion.show_popup(true)
   519 
   520             case None =>
   521           }
   522         case _ =>
   523       }
   524     }
   525 
   526 
   527     /* process key event */
   528 
   529     private def process(evt: KeyEvent)
   530     {
   531       if (PIDE.options.bool("jedit_completion")) {
   532         dismissed()
   533         if (evt.getKeyChar != '\b') {
   534           val special = JEdit_Lib.special_key(evt)
   535           if (PIDE.options.seconds("jedit_completion_delay").is_zero && !special) {
   536             process_delay.revoke()
   537             action()
   538           }
   539           else process_delay.invoke()
   540         }
   541       }
   542     }
   543 
   544     private val process_delay =
   545       Swing_Thread.delay_last(PIDE.options.seconds("jedit_completion_delay")) {
   546         action()
   547       }
   548 
   549     override def processKeyEvent(evt0: KeyEvent)
   550     {
   551       val evt = KeyEventWorkaround.processKeyEvent(evt0)
   552       if (evt != null) {
   553         evt.getID match {
   554           case KeyEvent.KEY_PRESSED =>
   555             val key_code = evt.getKeyCode
   556             if (key_code == KeyEvent.VK_ESCAPE) {
   557               if (dismissed()) evt.consume
   558             }
   559           case KeyEvent.KEY_TYPED =>
   560             super.processKeyEvent(evt)
   561             process(evt)
   562             evt.consume
   563           case _ =>
   564         }
   565         if (!evt.isConsumed) super.processKeyEvent(evt)
   566       }
   567     }
   568   }
   569 }
   570 
   571 
   572 class Completion_Popup private(
   573   opt_range: Option[Text.Range],
   574   layered: JLayeredPane,
   575   location: Point,
   576   font: Font,
   577   items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
   578 {
   579   completion =>
   580 
   581   Swing_Thread.require {}
   582 
   583   require(!items.isEmpty)
   584   val multi = items.length > 1
   585 
   586 
   587   /* actions */
   588 
   589   def complete(item: Completion.Item) { }
   590   def propagate(evt: KeyEvent) { }
   591   def shutdown(focus: Boolean) { }
   592 
   593 
   594   /* list view */
   595 
   596   private val list_view = new ListView(items)
   597   list_view.font = font
   598   list_view.selection.intervalMode = ListView.IntervalMode.Single
   599   list_view.peer.setFocusTraversalKeysEnabled(false)
   600   list_view.peer.setVisibleRowCount(items.length min 8)
   601   list_view.peer.setSelectedIndex(0)
   602 
   603   for (cond <-
   604     List(JComponent.WHEN_FOCUSED,
   605       JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT,
   606       JComponent.WHEN_IN_FOCUSED_WINDOW)) list_view.peer.setInputMap(cond, null)
   607 
   608   private def complete_selected(): Boolean =
   609   {
   610     list_view.selection.items.toList match {
   611       case item :: _ => complete(item.item); true
   612       case _ => false
   613     }
   614   }
   615 
   616   private def move_items(n: Int)
   617   {
   618     val i = list_view.peer.getSelectedIndex
   619     val j = ((i + n) min (items.length - 1)) max 0
   620     if (i != j) {
   621       list_view.peer.setSelectedIndex(j)
   622       list_view.peer.ensureIndexIsVisible(j)
   623     }
   624   }
   625 
   626   private def move_pages(n: Int)
   627   {
   628     val page_size = list_view.peer.getVisibleRowCount - 1
   629     move_items(page_size * n)
   630   }
   631 
   632 
   633   /* event handling */
   634 
   635   val inner_key_listener =
   636     JEdit_Lib.key_listener(
   637       key_pressed = (e: KeyEvent) =>
   638         {
   639           if (!e.isConsumed) {
   640             e.getKeyCode match {
   641               case KeyEvent.VK_TAB =>
   642                 if (complete_selected()) e.consume
   643                 hide_popup()
   644               case KeyEvent.VK_ESCAPE =>
   645                 hide_popup()
   646                 e.consume
   647               case KeyEvent.VK_UP | KeyEvent.VK_KP_UP if multi =>
   648                 move_items(-1)
   649                 e.consume
   650               case KeyEvent.VK_DOWN | KeyEvent.VK_KP_DOWN if multi =>
   651                 move_items(1)
   652                 e.consume
   653               case KeyEvent.VK_PAGE_UP if multi =>
   654                 move_pages(-1)
   655                 e.consume
   656               case KeyEvent.VK_PAGE_DOWN if multi =>
   657                 move_pages(1)
   658                 e.consume
   659               case _ =>
   660                 if (e.isActionKey || e.isAltDown || e.isMetaDown || e.isControlDown)
   661                   hide_popup()
   662             }
   663           }
   664           propagate(e)
   665         },
   666       key_typed = propagate _
   667     )
   668 
   669   list_view.peer.addKeyListener(inner_key_listener)
   670 
   671   list_view.peer.addMouseListener(new MouseAdapter {
   672     override def mouseClicked(e: MouseEvent) {
   673       if (complete_selected()) e.consume
   674       hide_popup()
   675     }
   676   })
   677 
   678   list_view.peer.addFocusListener(new FocusAdapter {
   679     override def focusLost(e: FocusEvent) { hide_popup() }
   680   })
   681 
   682 
   683   /* main content */
   684 
   685   override def getFocusTraversalKeysEnabled = false
   686   completion.setBorder(new LineBorder(Color.BLACK))
   687   completion.add((new ScrollPane(list_view)).peer.asInstanceOf[JComponent])
   688 
   689 
   690   /* popup */
   691 
   692   def active_range: Option[Text.Range] =
   693     if (isDisplayable) opt_range else None
   694 
   695   private val popup =
   696   {
   697     val screen = JEdit_Lib.screen_location(layered, location)
   698     val size =
   699     {
   700       val geometry = JEdit_Lib.window_geometry(completion, completion)
   701       val bounds = Rendering.popup_bounds
   702       val w = geometry.width min (screen.bounds.width * bounds).toInt min layered.getWidth
   703       val h = geometry.height min (screen.bounds.height * bounds).toInt min layered.getHeight
   704       new Dimension(w, h)
   705     }
   706     new Popup(layered, completion, screen.relative(layered, size), size)
   707   }
   708 
   709   private def show_popup(focus: Boolean)
   710   {
   711     popup.show
   712     if (focus) list_view.requestFocus
   713   }
   714 
   715   private def hide_popup()
   716   {
   717     shutdown(list_view.peer.isFocusOwner)
   718     popup.hide
   719   }
   720 }
   721