src/Pure/General/untyped.scala
changeset 63419 f473b6b16c63
parent 59080 611914621edb
child 64370 865b39487b5d
equal deleted inserted replaced
63409:3f3223b90239 63419:f473b6b16c63
     6 */
     6 */
     7 
     7 
     8 package isabelle
     8 package isabelle
     9 
     9 
    10 
    10 
    11 import java.lang.reflect.Method
    11 import java.lang.reflect.{Method, Field}
    12 
    12 
    13 
    13 
    14 object Untyped
    14 object Untyped
    15 {
    15 {
    16   def method(c: Class[_], name: String, arg_types: Class[_]*): Method =
    16   def method(c: Class[_], name: String, arg_types: Class[_]*): Method =
    28       next_elem = c.getSuperclass.asInstanceOf[Class[_ <: AnyRef]]
    28       next_elem = c.getSuperclass.asInstanceOf[Class[_ <: AnyRef]]
    29       c
    29       c
    30     }
    30     }
    31   }
    31   }
    32 
    32 
       
    33   def field(obj: AnyRef, x: String): Field =
       
    34   {
       
    35     val iterator =
       
    36       for {
       
    37         c <- classes(obj)
       
    38         field <- c.getDeclaredFields.iterator
       
    39         if field.getName == x
       
    40       } yield {
       
    41         field.setAccessible(true)
       
    42         field
       
    43       }
       
    44     if (iterator.hasNext) iterator.next
       
    45     else error("No field " + quote(x) + " for " + obj)
       
    46   }
       
    47 
    33   def get[A](obj: AnyRef, x: String): A =
    48   def get[A](obj: AnyRef, x: String): A =
    34     if (obj == null) null.asInstanceOf[A]
    49     if (obj == null) null.asInstanceOf[A]
    35     else {
    50     else field(obj, x).get(obj).asInstanceOf[A]
    36       val iterator =
    51 
    37         for {
    52   def set[A](obj: AnyRef, x: String, y: A): Unit =
    38           c <- classes(obj)
    53     field(obj, x).set(obj, y)
    39           field <- c.getDeclaredFields.iterator
       
    40           if field.getName == x
       
    41         } yield {
       
    42           field.setAccessible(true)
       
    43           field.get(obj)
       
    44         }
       
    45       if (iterator.hasNext) iterator.next.asInstanceOf[A]
       
    46       else error("No field " + quote(x) + " for " + obj)
       
    47     }
       
    48 }
    54 }
    49