# HG changeset patch
# User wenzelm
# Date 1413308321 -7200
# Node ID 542fa5093ebf17722cbbf809301bc20f2b910ade
# Parent  a478a0742a8e671fb03e2f254b279ada5906ac80
access class hierarchy;
smash access to null;

diff -r a478a0742a8e -r 542fa5093ebf src/Pure/General/untyped.scala
--- a/src/Pure/General/untyped.scala	Tue Oct 14 08:23:23 2014 +0200
+++ b/src/Pure/General/untyped.scala	Tue Oct 14 19:38:41 2014 +0200
@@ -10,14 +10,30 @@
 
 object Untyped
 {
-  def get(obj: AnyRef, x: String): AnyRef =
-  {
-    obj.getClass.getDeclaredFields.find(_.getName == x) match {
-      case Some(field) =>
-        field.setAccessible(true)
-        field.get(obj)
-      case None => error("No field " + quote(x) + " for " + obj)
+  def classes(obj: AnyRef): Iterator[Class[_ <: AnyRef]] = new Iterator[Class[_ <: AnyRef]] {
+    private var next_elem: Class[_ <: AnyRef] = obj.getClass
+    def hasNext(): Boolean = next_elem != null
+    def next(): Class[_ <: AnyRef] = {
+      val c = next_elem
+      next_elem = c.getSuperclass.asInstanceOf[Class[_ <: AnyRef]]
+      c
     }
   }
+
+  def get(obj: AnyRef, x: String): AnyRef =
+    if (obj == null) null
+    else {
+      val iterator =
+        for {
+          c <- classes(obj)
+          field <- c.getDeclaredFields.iterator
+          if field.getName == x
+        } yield {
+          field.setAccessible(true)
+          field.get(obj)
+        }
+      if (iterator.hasNext) iterator.next
+      else error("No field " + quote(x) + " for " + obj)
+    }
 }