dismiss popups more uniformly;
authorwenzelm
Wed Aug 28 09:36:05 2013 +0200 (2013-08-28 ago)
changeset 53244ec6011bf2362
parent 53243 dabe46c68228
child 53245 301b69957af7
dismiss popups more uniformly;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/plugin.scala
src/Tools/jEdit/src/pretty_text_area.scala
     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) =>
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Wed Aug 28 09:12:50 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Wed Aug 28 09:36:05 2013 +0200
     2.3 @@ -154,7 +154,7 @@
     2.4        key_typed = Completion_Popup.Text_Area.input(text_area, PIDE.get_recent_syntax, _),
     2.5        key_pressed = (evt: KeyEvent) =>
     2.6          {
     2.7 -          if (evt.getKeyCode == KeyEvent.VK_ESCAPE && Pretty_Tooltip.dismissed_all())
     2.8 +          if (evt.getKeyCode == KeyEvent.VK_ESCAPE && PIDE.dismissed_popups(text_area.getView))
     2.9              evt.consume
    2.10          }
    2.11      )
     3.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Aug 28 09:12:50 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Aug 28 09:36:05 2013 +0200
     3.3 @@ -53,6 +53,16 @@
     3.4    lazy val editor = new JEdit_Editor
     3.5  
     3.6  
     3.7 +  /* popups */
     3.8 +
     3.9 +  def dismissed_popups(view: View): Boolean =
    3.10 +  {
    3.11 +    val b1 = Completion_Popup.dismissed_view(view)
    3.12 +    val b2 = Pretty_Tooltip.dismissed_all()
    3.13 +    b1 || b2
    3.14 +  }
    3.15 +
    3.16 +
    3.17    /* document model and view */
    3.18  
    3.19    def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
    3.20 @@ -265,7 +275,7 @@
    3.21                  PIDE.init_view(buffer, text_area)
    3.22              }
    3.23              else {
    3.24 -              Pretty_Tooltip.dismissed_all()
    3.25 +              PIDE.dismissed_popups(text_area.getView)
    3.26                PIDE.exit_view(buffer, text_area)
    3.27              }
    3.28            }
     4.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Wed Aug 28 09:12:50 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Wed Aug 28 09:36:05 2013 +0200
     4.3 @@ -177,7 +177,7 @@
     4.4              evt.consume
     4.5  
     4.6            case KeyEvent.VK_ESCAPE =>
     4.7 -            if (Pretty_Tooltip.dismissed_all()) evt.consume
     4.8 +            if (PIDE.dismissed_popups(view)) evt.consume
     4.9  
    4.10            case _ =>
    4.11          }