some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;
authorwenzelm
Sun Jul 07 18:04:46 2013 +0200 (2013-07-07)
changeset 52548a1a8248a4677
parent 52547 0ddcfc0d05d4
child 52549 802576856527
some attempts to avoid sandwiching of actions stemming from single ESCAPE key event, to avoid potential conflict with ongoing text selection;
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/pretty_text_area.scala
src/Tools/jEdit/src/pretty_tooltip.scala
src/Tools/jEdit/src/rich_text_area.scala
     1.1 --- a/src/Tools/jEdit/src/document_view.scala	Sun Jul 07 17:52:13 2013 +0200
     1.2 +++ b/src/Tools/jEdit/src/document_view.scala	Sun Jul 07 18:04:46 2013 +0200
     1.3 @@ -152,7 +152,8 @@
     1.4    private val key_listener = new KeyAdapter {
     1.5      override def keyTyped(evt: KeyEvent)
     1.6      {
     1.7 -      if (evt.getKeyChar == 27) Pretty_Tooltip.dismiss_all()
     1.8 +      if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all())
     1.9 +        evt.consume
    1.10      }
    1.11    }
    1.12  
     2.1 --- a/src/Tools/jEdit/src/pretty_text_area.scala	Sun Jul 07 17:52:13 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/pretty_text_area.scala	Sun Jul 07 18:04:46 2013 +0200
     2.3 @@ -178,7 +178,8 @@
     2.4  
     2.5      override def keyTyped(evt: KeyEvent)
     2.6      {
     2.7 -      if (evt.getKeyChar == 27) Pretty_Tooltip.dismiss_all()
     2.8 +      if (evt.getKeyChar == 27 && Pretty_Tooltip.dismissed_all())
     2.9 +        evt.consume
    2.10  
    2.11        if (propagate_keys && !evt.isConsumed)
    2.12          view.getInputHandler.processKeyEvent(evt, View.ACTION_BAR, false)
     3.1 --- a/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Jul 07 17:52:13 2013 +0200
     3.2 +++ b/src/Tools/jEdit/src/pretty_tooltip.scala	Sun Jul 07 18:04:46 2013 +0200
     3.3 @@ -117,12 +117,14 @@
     3.4      }
     3.5    }
     3.6  
     3.7 -  def dismiss_all()
     3.8 -  {
     3.9 -    deactivate()
    3.10 -    stack.foreach(_.hide_popup)
    3.11 -    stack = Nil
    3.12 -  }
    3.13 +  def dismissed_all(): Boolean =
    3.14 +    if (stack.isEmpty) false
    3.15 +    else {
    3.16 +      deactivate()
    3.17 +      stack.foreach(_.hide_popup)
    3.18 +      stack = Nil
    3.19 +      true
    3.20 +    }
    3.21  
    3.22  
    3.23    /* auxiliary geometry measurement */
     4.1 --- a/src/Tools/jEdit/src/rich_text_area.scala	Sun Jul 07 17:52:13 2013 +0200
     4.2 +++ b/src/Tools/jEdit/src/rich_text_area.scala	Sun Jul 07 18:04:46 2013 +0200
     4.3 @@ -156,7 +156,7 @@
     4.4        robust_body(()) {
     4.5          hyperlink_area.info match {
     4.6            case Some(Text.Info(_, link)) =>
     4.7 -            Pretty_Tooltip.dismiss_all()
     4.8 +            Pretty_Tooltip.dismissed_all()
     4.9              link.follow(view)
    4.10            case None =>
    4.11          }