src/Pure/Tools/spell_checker.scala
changeset 73909 1d0d9772fff0
parent 73367 77ef8bef0593
child 75393 87ebf5a50283
--- a/src/Pure/Tools/spell_checker.scala	Wed Jun 30 21:35:30 2021 +0200
+++ b/src/Pure/Tools/spell_checker.scala	Wed Jun 30 22:14:27 2021 +0200
@@ -9,6 +9,7 @@
 
 
 import java.lang.Class
+import java.util.{List => JList}
 
 import scala.collection.mutable
 import scala.annotation.tailrec
@@ -223,7 +224,7 @@
   {
     val res =
       Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
-        invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
+        invoke(dict, word).asInstanceOf[JList[AnyRef]].toArray.toList.map(_.toString)
     if (res.isEmpty) None else Some(res)
   }