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