src/Tools/jEdit/src/completion_popup.scala
changeset 53244 ec6011bf2362
parent 53243 dabe46c68228
child 53246 8d34caf5bf82
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 09:12:50 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Aug 28 09:36:05 2013 +0200
     1.3 @@ -28,16 +28,28 @@
     1.4    { override def toString: String = description }
     1.5  
     1.6  
     1.7 -  /* register single instance within root */
     1.8 +  /* single instance within root */
     1.9 +
    1.10 +  def dismissed_view(view: View): Boolean = dismissed(view.getRootPane)
    1.11 +
    1.12 +  private def dismissed(root: JComponent): Boolean =
    1.13 +  {
    1.14 +    Swing_Thread.require()
    1.15 +
    1.16 +    root.getClientProperty(Completion_Popup) match {
    1.17 +      case old_completion: Completion_Popup =>
    1.18 +        old_completion.hide_popup
    1.19 +        true
    1.20 +      case _ =>
    1.21 +        false
    1.22 +    }
    1.23 +  }
    1.24  
    1.25    private def register(root: JComponent, completion: Completion_Popup)
    1.26    {
    1.27      Swing_Thread.require()
    1.28  
    1.29 -    root.getClientProperty(Completion_Popup) match {
    1.30 -      case old_completion: Completion_Popup => old_completion.hide_popup
    1.31 -      case _ =>
    1.32 -    }
    1.33 +    dismissed(root)
    1.34      root.putClientProperty(Completion_Popup, completion)
    1.35    }
    1.36  
    1.37 @@ -69,13 +81,13 @@
    1.38      {
    1.39        Swing_Thread.require()
    1.40  
    1.41 +      dismissed(text_area)
    1.42 +
    1.43        val view = text_area.getView
    1.44        val root = view.getRootPane
    1.45        val buffer = text_area.getBuffer
    1.46        val painter = text_area.getPainter
    1.47  
    1.48 -      register(root, null)
    1.49 -
    1.50        if (buffer.isEditable && !evt.isConsumed) {
    1.51          get_syntax match {
    1.52            case Some(syntax) =>