tuned;
authorwenzelm
Wed, 16 Apr 2014 13:48:35 +0200
changeset 56605 46313aafaf87
parent 56604 1b153b989860
child 56606 68b7a6db4a32
tuned;
src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Wed Apr 16 13:35:49 2014 +0200
+++ b/src/Tools/jEdit/src/completion_popup.scala	Wed Apr 16 13:48:35 2014 +0200
@@ -110,11 +110,7 @@
 
     def active_range: Option[Text.Range] =
       completion_popup match {
-        case Some(completion) =>
-          completion.active_range match {
-            case Some(range) if completion.isDisplayable => Some(range)
-            case _ => None
-          }
+        case Some(completion) => completion.active_range
         case None => None
       }
 
@@ -571,7 +567,7 @@
 
 
 class Completion_Popup private(
-  val active_range: Option[Text.Range],
+  opt_range: Option[Text.Range],
   layered: JLayeredPane,
   location: Point,
   font: Font,
@@ -690,6 +686,9 @@
 
   /* popup */
 
+  def active_range: Option[Text.Range] =
+    if (isDisplayable) opt_range else None
+
   private val popup =
   {
     val screen = JEdit_Lib.screen_location(layered, location)