tuned signature -- weaker type requirement;
authorwenzelm
Mon Feb 24 12:23:35 2014 +0100 (2014-02-24)
changeset 55712e757e8c8d8ea
parent 55711 9e3d64e5919a
child 55713 734ac5709fbe
tuned signature -- weaker type requirement;
src/Tools/jEdit/src/completion_popup.scala
src/Tools/jEdit/src/document_view.scala
src/Tools/jEdit/src/plugin.scala
     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 {
     2.1 --- a/src/Tools/jEdit/src/document_view.scala	Mon Feb 24 12:14:03 2014 +0100
     2.2 +++ b/src/Tools/jEdit/src/document_view.scala	Mon Feb 24 12:23:35 2014 +0100
     2.3 @@ -18,7 +18,7 @@
     2.4  
     2.5  import org.gjt.sp.jedit.jEdit
     2.6  import org.gjt.sp.jedit.options.GutterOptionPane
     2.7 -import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
     2.8 +import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
     2.9  
    2.10  
    2.11  object Document_View
    2.12 @@ -27,7 +27,7 @@
    2.13  
    2.14    private val key = new Object
    2.15  
    2.16 -  def apply(text_area: JEditTextArea): Option[Document_View] =
    2.17 +  def apply(text_area: TextArea): Option[Document_View] =
    2.18    {
    2.19      Swing_Thread.require()
    2.20      text_area.getClientProperty(key) match {
     3.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Feb 24 12:14:03 2014 +0100
     3.2 +++ b/src/Tools/jEdit/src/plugin.scala	Mon Feb 24 12:23:35 2014 +0100
     3.3 @@ -68,7 +68,7 @@
     3.4  
     3.5    def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
     3.6  
     3.7 -  def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
     3.8 +  def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area)
     3.9  
    3.10    def document_views(buffer: Buffer): List[Document_View] =
    3.11      for {