src/Tools/jEdit/src/completion_popup.scala
changeset 56605 46313aafaf87
parent 56593 0ea7c84110ac
child 56606 68b7a6db4a32
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Wed Apr 16 13:35:49 2014 +0200
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Apr 16 13:48:35 2014 +0200
     1.3 @@ -110,11 +110,7 @@
     1.4  
     1.5      def active_range: Option[Text.Range] =
     1.6        completion_popup match {
     1.7 -        case Some(completion) =>
     1.8 -          completion.active_range match {
     1.9 -            case Some(range) if completion.isDisplayable => Some(range)
    1.10 -            case _ => None
    1.11 -          }
    1.12 +        case Some(completion) => completion.active_range
    1.13          case None => None
    1.14        }
    1.15  
    1.16 @@ -571,7 +567,7 @@
    1.17  
    1.18  
    1.19  class Completion_Popup private(
    1.20 -  val active_range: Option[Text.Range],
    1.21 +  opt_range: Option[Text.Range],
    1.22    layered: JLayeredPane,
    1.23    location: Point,
    1.24    font: Font,
    1.25 @@ -690,6 +686,9 @@
    1.26  
    1.27    /* popup */
    1.28  
    1.29 +  def active_range: Option[Text.Range] =
    1.30 +    if (isDisplayable) opt_range else None
    1.31 +
    1.32    private val popup =
    1.33    {
    1.34      val screen = JEdit_Lib.screen_location(layered, location)