# HG changeset patch
# User wenzelm
# Date 1649239890 -7200
# Node ID 5640c4db7d378a62512a39611d4b48a0ded0a219
# Parent  e859c9f30db20735414cdd2e5122040219459286
more operations;
tuned message: Class.toString already says "class ...";

diff -r e859c9f30db2 -r 5640c4db7d37 src/Pure/General/untyped.scala
--- a/src/Pure/General/untyped.scala	Wed Apr 06 11:09:58 2022 +0200
+++ b/src/Pure/General/untyped.scala	Wed Apr 06 12:11:30 2022 +0200
@@ -17,6 +17,16 @@
     con
   }
 
+  def the_constructor[C](c:  Class[C]): Constructor[C] = {
+    c.getDeclaredConstructors().toList match {
+      case List(con) =>
+        con.setAccessible(true)
+        con.asInstanceOf[Constructor[C]]
+      case Nil => error("No constructor for " + c)
+      case _ => error("Multiple constructors for " + c)
+    }
+  }
+
   def method(c: Class[_], name: String, arg_types: Class[_]*): Method = {
     val m = c.getDeclaredMethod(name, arg_types: _*)
     m.setAccessible(true)
@@ -28,7 +38,7 @@
       case List(m) =>
         m.setAccessible(true)
         m
-      case Nil => error("Missing method " + quote(name) + " for " + c)
+      case Nil => error("No method " + quote(name) + " for " + c)
       case _ => error("Multiple methods " + quote(name) + " for " + c)
     }
   }
@@ -57,6 +67,9 @@
     else error("No field " + quote(x) + " for " + c0)
   }
 
+  def get_static[A](c: Class[_ <: AnyRef], x: String): A =
+    class_field(c, x).get(null).asInstanceOf[A]
+
   def field(obj: AnyRef, x: String): Field = class_field(obj.getClass, x)
 
   def get[A](obj: AnyRef, x: String): A =