src/Tools/jEdit/src/completion_popup.scala
changeset 55712 e757e8c8d8ea
parent 55711 9e3d64e5919a
child 55747 bef19c929ba5
     1.1 --- a/src/Tools/jEdit/src/completion_popup.scala	Mon Feb 24 12:14:03 2014 +0100
     1.2 +++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Feb 24 12:23:35 2014 +0100
     1.3 @@ -19,7 +19,7 @@
     1.4  import scala.swing.event.MouseClicked
     1.5  
     1.6  import org.gjt.sp.jedit.View
     1.7 -import org.gjt.sp.jedit.textarea.{TextArea, JEditTextArea}
     1.8 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
     1.9  import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
    1.10  
    1.11  
    1.12 @@ -31,20 +31,19 @@
    1.13    {
    1.14      private val key = new Object
    1.15  
    1.16 -    def apply(text_area: JEditTextArea): Option[Completion_Popup.Text_Area] =
    1.17 +    def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
    1.18 +    {
    1.19 +      Swing_Thread.require()
    1.20        text_area.getClientProperty(key) match {
    1.21          case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
    1.22          case _ => None
    1.23        }
    1.24 +    }
    1.25  
    1.26 -    def active_range(text_area0: TextArea): Option[Text.Range] =
    1.27 -      text_area0 match {
    1.28 -        case text_area: JEditTextArea =>
    1.29 -          apply(text_area) match {
    1.30 -            case Some(text_area_completion) => text_area_completion.active_range
    1.31 -            case None => None
    1.32 -          }
    1.33 -        case _ => None
    1.34 +    def active_range(text_area: TextArea): Option[Text.Range] =
    1.35 +      apply(text_area) match {
    1.36 +        case Some(text_area_completion) => text_area_completion.active_range
    1.37 +        case None => None
    1.38        }
    1.39  
    1.40      def exit(text_area: JEditTextArea)
    1.41 @@ -67,7 +66,7 @@
    1.42        text_area_completion
    1.43      }
    1.44  
    1.45 -    def dismissed(text_area: JEditTextArea): Boolean =
    1.46 +    def dismissed(text_area: TextArea): Boolean =
    1.47      {
    1.48        Swing_Thread.require()
    1.49        apply(text_area) match {