--- 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)