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