src/Tools/jEdit/src/completion_popup.scala
changeset 53272 0dfd78ff7696
parent 53247 bd595338ca18
child 53273 473ea1ed7503
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 09:16:03 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Thu Aug 29 10:01:59 2013 +0200
     1.3 @@ -28,35 +28,33 @@
     1.4    { override def toString: String = description }
     1.5  
     1.6  
     1.7 -  /* maintain single instance */
     1.8 -
     1.9 -  def dismissed(layered: JLayeredPane): Boolean =
    1.10 -  {
    1.11 -    Swing_Thread.require()
    1.12 -
    1.13 -    layered.getClientProperty(Completion_Popup) match {
    1.14 -      case old_completion: Completion_Popup =>
    1.15 -        old_completion.hide_popup()
    1.16 -        true
    1.17 -      case _ =>
    1.18 -        false
    1.19 -    }
    1.20 -  }
    1.21 -
    1.22 -  private def register(layered: JLayeredPane, completion: Completion_Popup)
    1.23 -  {
    1.24 -    Swing_Thread.require()
    1.25 -
    1.26 -    dismissed(layered)
    1.27 -    layered.putClientProperty(Completion_Popup, completion)
    1.28 -  }
    1.29 -
    1.30 -
    1.31 -  /* jEdit text area operations */
    1.32 +  /* setup for jEdit text area */
    1.33  
    1.34    object Text_Area
    1.35    {
    1.36 -    private def insert(text_area: JEditTextArea, item: Item)
    1.37 +    def apply(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax]): Text_Area =
    1.38 +      new Text_Area(text_area, get_syntax)
    1.39 +  }
    1.40 +
    1.41 +  class Text_Area private(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax])
    1.42 +  {
    1.43 +    private var completion_popup: Option[Completion_Popup] = None
    1.44 +
    1.45 +    def dismissed(): Boolean =
    1.46 +    {
    1.47 +      Swing_Thread.require()
    1.48 +
    1.49 +      completion_popup match {
    1.50 +        case Some(completion) =>
    1.51 +          completion.hide_popup()
    1.52 +          completion_popup = None
    1.53 +          true
    1.54 +        case None =>
    1.55 +          false
    1.56 +      }
    1.57 +    }
    1.58 +
    1.59 +    private def insert(item: Item)
    1.60      {
    1.61        Swing_Thread.require()
    1.62  
    1.63 @@ -75,7 +73,7 @@
    1.64        }
    1.65      }
    1.66  
    1.67 -    def input(text_area: JEditTextArea, get_syntax: => Option[Outer_Syntax], evt: KeyEvent)
    1.68 +    def input(evt: KeyEvent)
    1.69      {
    1.70        Swing_Thread.require()
    1.71  
    1.72 @@ -85,7 +83,7 @@
    1.73        val painter = text_area.getPainter
    1.74  
    1.75        if (buffer.isEditable && !evt.isConsumed) {
    1.76 -        dismissed(layered)
    1.77 +        dismissed()
    1.78  
    1.79          get_syntax match {
    1.80            case Some(syntax) =>
    1.81 @@ -109,10 +107,7 @@
    1.82              }
    1.83              result match {
    1.84                case Some((original, items)) =>
    1.85 -                val popup_font =
    1.86 -                  painter.getFont.deriveFont(
    1.87 -                    (painter.getFont.getSize2D * PIDE.options.real("jedit_popup_font_scale")).toFloat
    1.88 -                      max 10.0f)
    1.89 +                val font = painter.getFont.deriveFont(Rendering.font_size("jedit_popup_font_scale"))
    1.90  
    1.91                  val loc1 = text_area.offsetToXY(caret - original.length)
    1.92                  if (loc1 != null) {
    1.93 @@ -120,15 +115,15 @@
    1.94                      SwingUtilities.convertPoint(painter,
    1.95                        loc1.x, loc1.y + painter.getFontMetrics.getHeight, layered)
    1.96                    val completion =
    1.97 -                    new Completion_Popup(layered, loc2, popup_font, items) {
    1.98 -                      override def complete(item: Item) { insert(text_area, item) }
    1.99 +                    new Completion_Popup(layered, loc2, font, items) {
   1.100 +                      override def complete(item: Item) { insert(item) }
   1.101                        override def propagate(e: KeyEvent) {
   1.102                          JEdit_Lib.propagate_key(view, e)
   1.103 -                        input(text_area, get_syntax, e)
   1.104 +                        input(e)
   1.105                        }
   1.106                        override def refocus() { text_area.requestFocus }
   1.107                      }
   1.108 -                  register(layered, completion)
   1.109 +                  completion_popup = Some(completion)
   1.110                    completion.show_popup()
   1.111                  }
   1.112                case None =>
   1.113 @@ -144,7 +139,7 @@
   1.114  class Completion_Popup private(
   1.115    layered: JLayeredPane,
   1.116    location: Point,
   1.117 -  popup_font: Font,
   1.118 +  font: Font,
   1.119    items: List[Completion_Popup.Item]) extends JPanel(new BorderLayout)
   1.120  {
   1.121    completion =>
   1.122 @@ -163,9 +158,7 @@
   1.123    /* list view */
   1.124  
   1.125    private val list_view = new ListView(items)
   1.126 -  {
   1.127 -    font = popup_font
   1.128 -  }
   1.129 +  list_view.font = font
   1.130    list_view.selection.intervalMode = ListView.IntervalMode.Single
   1.131    list_view.peer.setFocusTraversalKeysEnabled(false)
   1.132    list_view.peer.setVisibleRowCount(items.length min 8)