# HG changeset patch
# User wenzelm
# Date 1649236198 -7200
# Node ID e859c9f30db20735414cdd2e5122040219459286
# Parent  c7051638a38cca478f80b171fa5669a824fbc25b
clarified signature;

diff -r c7051638a38c -r e859c9f30db2 src/Pure/General/untyped.scala
--- a/src/Pure/General/untyped.scala	Mon Apr 04 23:50:40 2022 +0200
+++ b/src/Pure/General/untyped.scala	Wed Apr 06 11:09:58 2022 +0200
@@ -23,8 +23,18 @@
     m
   }
 
-  def classes(obj: AnyRef): Iterator[Class[_ <: AnyRef]] = new Iterator[Class[_ <: AnyRef]] {
-    private var next_elem: Class[_ <: AnyRef] = obj.getClass
+  def the_method(c: Class[_], name: String): Method = {
+    c.getDeclaredMethods().iterator.filter(m => m.getName == name).toList match {
+      case List(m) =>
+        m.setAccessible(true)
+        m
+      case Nil => error("Missing method " + quote(name) + " for " + c)
+      case _ => error("Multiple methods " + quote(name) + " for " + c)
+    }
+  }
+
+  def classes(c0: Class[_ <: AnyRef]): Iterator[Class[_ <: AnyRef]] = new Iterator[Class[_ <: AnyRef]] {
+    private var next_elem: Class[_ <: AnyRef] = c0
     def hasNext: Boolean = next_elem != null
     def next(): Class[_ <: AnyRef] = {
       val c = next_elem
@@ -33,10 +43,10 @@
     }
   }
 
-  def field(obj: AnyRef, x: String): Field = {
+  def class_field(c0: Class[_ <: AnyRef], x: String): Field = {
     val iterator =
       for {
-        c <- classes(obj)
+        c <- classes(c0)
         field <- c.getDeclaredFields.iterator
         if field.getName == x
       } yield {
@@ -44,9 +54,11 @@
         field
       }
     if (iterator.hasNext) iterator.next()
-    else error("No field " + quote(x) + " for " + obj)
+    else error("No field " + quote(x) + " for " + c0)
   }
 
+  def field(obj: AnyRef, x: String): Field = class_field(obj.getClass, x)
+
   def get[A](obj: AnyRef, x: String): A =
     if (obj == null) null.asInstanceOf[A]
     else field(obj, x).get(obj).asInstanceOf[A]