src/Tools/jEdit/src/completion_popup.scala
changeset 53851 86c8f15afd88
parent 53848 8d7029eb0c31
child 53987 16a0cd5293d9
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Tue Sep 24 19:53:05 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Tue Sep 24 19:57:44 2013 +0200
     1.3 @@ -281,10 +281,8 @@
     1.4                val fm = text_field.getFontMetrics(text_field.getFont)
     1.5                val loc =
     1.6                  SwingUtilities.convertPoint(text_field, fm.stringWidth(text), fm.getHeight, layered)
     1.7 -              val font =
     1.8 -                text_field.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
     1.9  
    1.10 -              val completion = new Completion_Popup(layered, loc, font, result.items)
    1.11 +              val completion = new Completion_Popup(layered, loc, text_field.getFont, result.items)
    1.12                {
    1.13                  override def complete(item: Completion.Item) {
    1.14                    PIDE.completion_history.update(item)