# HG changeset patch
# User wenzelm
# Date 1393241015 -3600
# Node ID e757e8c8d8ea4878d44dedfc7a265cbdf4adb583
# Parent  9e3d64e5919a4929565a677a7ce93b3f51fec71f
tuned signature -- weaker type requirement;

diff -r 9e3d64e5919a -r e757e8c8d8ea src/Tools/jEdit/src/completion_popup.scala
--- a/src/Tools/jEdit/src/completion_popup.scala	Mon Feb 24 12:14:03 2014 +0100
+++ b/src/Tools/jEdit/src/completion_popup.scala	Mon Feb 24 12:23:35 2014 +0100
@@ -19,7 +19,7 @@
 import scala.swing.event.MouseClicked
 
 import org.gjt.sp.jedit.View
-import org.gjt.sp.jedit.textarea.{TextArea, JEditTextArea}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
 import org.gjt.sp.jedit.gui.{HistoryTextField, KeyEventWorkaround}
 
 
@@ -31,20 +31,19 @@
   {
     private val key = new Object
 
-    def apply(text_area: JEditTextArea): Option[Completion_Popup.Text_Area] =
+    def apply(text_area: TextArea): Option[Completion_Popup.Text_Area] =
+    {
+      Swing_Thread.require()
       text_area.getClientProperty(key) match {
         case text_area_completion: Completion_Popup.Text_Area => Some(text_area_completion)
         case _ => None
       }
+    }
 
-    def active_range(text_area0: TextArea): Option[Text.Range] =
-      text_area0 match {
-        case text_area: JEditTextArea =>
-          apply(text_area) match {
-            case Some(text_area_completion) => text_area_completion.active_range
-            case None => None
-          }
-        case _ => None
+    def active_range(text_area: TextArea): Option[Text.Range] =
+      apply(text_area) match {
+        case Some(text_area_completion) => text_area_completion.active_range
+        case None => None
       }
 
     def exit(text_area: JEditTextArea)
@@ -67,7 +66,7 @@
       text_area_completion
     }
 
-    def dismissed(text_area: JEditTextArea): Boolean =
+    def dismissed(text_area: TextArea): Boolean =
     {
       Swing_Thread.require()
       apply(text_area) match {
diff -r 9e3d64e5919a -r e757e8c8d8ea src/Tools/jEdit/src/document_view.scala
--- a/src/Tools/jEdit/src/document_view.scala	Mon Feb 24 12:14:03 2014 +0100
+++ b/src/Tools/jEdit/src/document_view.scala	Mon Feb 24 12:23:35 2014 +0100
@@ -18,7 +18,7 @@
 
 import org.gjt.sp.jedit.jEdit
 import org.gjt.sp.jedit.options.GutterOptionPane
-import org.gjt.sp.jedit.textarea.{JEditTextArea, TextAreaExtension, TextAreaPainter}
+import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea, TextAreaExtension, TextAreaPainter}
 
 
 object Document_View
@@ -27,7 +27,7 @@
 
   private val key = new Object
 
-  def apply(text_area: JEditTextArea): Option[Document_View] =
+  def apply(text_area: TextArea): Option[Document_View] =
   {
     Swing_Thread.require()
     text_area.getClientProperty(key) match {
diff -r 9e3d64e5919a -r e757e8c8d8ea src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Mon Feb 24 12:14:03 2014 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Feb 24 12:23:35 2014 +0100
@@ -68,7 +68,7 @@
 
   def document_model(buffer: Buffer): Option[Document_Model] = Document_Model(buffer)
 
-  def document_view(text_area: JEditTextArea): Option[Document_View] = Document_View(text_area)
+  def document_view(text_area: TextArea): Option[Document_View] = Document_View(text_area)
 
   def document_views(buffer: Buffer): List[Document_View] =
     for {