# HG changeset patch
# User wenzelm
# Date 1608583992 -3600
# Node ID fc69884a6e5a9f5b146eafb655161a5d64a45196
# Parent  31ff3c9629372c22f59921b66fbafb6003f62805
clarified modules;

diff -r 31ff3c962937 -r fc69884a6e5a src/Pure/General/untyped.scala
--- a/src/Pure/General/untyped.scala	Mon Dec 21 14:03:12 2020 +0100
+++ b/src/Pure/General/untyped.scala	Mon Dec 21 21:53:12 2020 +0100
@@ -7,11 +7,18 @@
 package isabelle
 
 
-import java.lang.reflect.{Method, Field}
+import java.lang.reflect.{Constructor, Method, Field}
 
 
 object Untyped
 {
+  def constructor[C](c: Class[C], arg_types: Class[_]*): Constructor[C] =
+  {
+    val con = c.getDeclaredConstructor(arg_types: _*)
+    con.setAccessible(true)
+    con
+  }
+
   def method(c: Class[_], name: String, arg_types: Class[_]*): Method =
   {
     val m = c.getDeclaredMethod(name, arg_types: _*)
diff -r 31ff3c962937 -r fc69884a6e5a src/Pure/Tools/spell_checker.scala
--- a/src/Pure/Tools/spell_checker.scala	Mon Dec 21 14:03:12 2020 +0100
+++ b/src/Pure/Tools/spell_checker.scala	Mon Dec 21 21:53:12 2020 +0100
@@ -141,9 +141,7 @@
         permanent_updates
 
     val factory_class = Class.forName("com.inet.jortho.DictionaryFactory")
-    val factory_constructor = factory_class.getConstructor()
-    factory_constructor.setAccessible(true)
-    val factory = factory_constructor.newInstance()
+    val factory = Untyped.constructor(factory_class).newInstance()
 
     val add = Untyped.method(factory_class, "add", classOf[String])