src/Pure/General/untyped.scala
author wenzelm
Tue Oct 14 19:38:41 2014 +0200 (2014-10-14)
changeset 58682 542fa5093ebf
parent 56905 fb38a767a78b
child 59079 12a689755c3d
permissions -rw-r--r--
access class hierarchy;
smash access to null;
     1 /*  Title:      Pure/General/untyped.scala
     2     Module:     PIDE
     3     Author:     Makarius
     4 
     5 Untyped, unscoped, unchecked access to JVM objects.
     6 */
     7 
     8 package isabelle
     9 
    10 
    11 object Untyped
    12 {
    13   def classes(obj: AnyRef): Iterator[Class[_ <: AnyRef]] = new Iterator[Class[_ <: AnyRef]] {
    14     private var next_elem: Class[_ <: AnyRef] = obj.getClass
    15     def hasNext(): Boolean = next_elem != null
    16     def next(): Class[_ <: AnyRef] = {
    17       val c = next_elem
    18       next_elem = c.getSuperclass.asInstanceOf[Class[_ <: AnyRef]]
    19       c
    20     }
    21   }
    22 
    23   def get(obj: AnyRef, x: String): AnyRef =
    24     if (obj == null) null
    25     else {
    26       val iterator =
    27         for {
    28           c <- classes(obj)
    29           field <- c.getDeclaredFields.iterator
    30           if field.getName == x
    31         } yield {
    32           field.setAccessible(true)
    33           field.get(obj)
    34         }
    35       if (iterator.hasNext) iterator.next
    36       else error("No field " + quote(x) + " for " + obj)
    37     }
    38 }
    39