clarified modules;
authorwenzelm
Mon, 21 Dec 2020 21:53:12 +0100
changeset 72973 fc69884a6e5a
parent 72972 31ff3c962937
child 72974 3afd293347cc
clarified modules;
src/Pure/General/untyped.scala
src/Pure/Tools/spell_checker.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: _*)
--- 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])