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