10Sstevel@tonic-gate/* Title: Pure/General/untyped.scala 20Sstevel@tonic-gate Author: Makarius 30Sstevel@tonic-gate 40Sstevel@tonic-gateUntyped, unscoped, unchecked access to JVM objects. 50Sstevel@tonic-gate*/ 60Sstevel@tonic-gate 70Sstevel@tonic-gatepackage isabelle 80Sstevel@tonic-gate 90Sstevel@tonic-gate 100Sstevel@tonic-gateimport java.lang.reflect.{Method, Field} 110Sstevel@tonic-gate 120Sstevel@tonic-gate 130Sstevel@tonic-gateobject Untyped 140Sstevel@tonic-gate{ 150Sstevel@tonic-gate def method(c: Class[_], name: String, arg_types: Class[_]*): Method = 160Sstevel@tonic-gate { 170Sstevel@tonic-gate val m = c.getDeclaredMethod(name, arg_types: _*) 180Sstevel@tonic-gate m.setAccessible(true) 190Sstevel@tonic-gate m 200Sstevel@tonic-gate } 210Sstevel@tonic-gate 220Sstevel@tonic-gate def classes(obj: AnyRef): Iterator[Class[_ <: AnyRef]] = new Iterator[Class[_ <: AnyRef]] { 230Sstevel@tonic-gate private var next_elem: Class[_ <: AnyRef] = obj.getClass 240Sstevel@tonic-gate def hasNext(): Boolean = next_elem != null 250Sstevel@tonic-gate def next(): Class[_ <: AnyRef] = { 260Sstevel@tonic-gate val c = next_elem 270Sstevel@tonic-gate next_elem = c.getSuperclass.asInstanceOf[Class[_ <: AnyRef]] 280Sstevel@tonic-gate c 290Sstevel@tonic-gate } 300Sstevel@tonic-gate } 310Sstevel@tonic-gate 320Sstevel@tonic-gate def field(obj: AnyRef, x: String): Field = 330Sstevel@tonic-gate { 340Sstevel@tonic-gate val iterator = 350Sstevel@tonic-gate for { 360Sstevel@tonic-gate c <- classes(obj) 370Sstevel@tonic-gate field <- c.getDeclaredFields.iterator 380Sstevel@tonic-gate if field.getName == x 390Sstevel@tonic-gate } yield { 400Sstevel@tonic-gate field.setAccessible(true) 410Sstevel@tonic-gate field 420Sstevel@tonic-gate } 430Sstevel@tonic-gate if (iterator.hasNext) iterator.next 440Sstevel@tonic-gate else error("No field " + quote(x) + " for " + obj) 450Sstevel@tonic-gate } 460Sstevel@tonic-gate 470Sstevel@tonic-gate def get[A](obj: AnyRef, x: String): A = 480Sstevel@tonic-gate if (obj == null) null.asInstanceOf[A] 490Sstevel@tonic-gate else field(obj, x).get(obj).asInstanceOf[A] 500Sstevel@tonic-gate 510Sstevel@tonic-gate def set[A](obj: AnyRef, x: String, y: A): Unit = 520Sstevel@tonic-gate field(obj, x).set(obj, y) 530Sstevel@tonic-gate} 540Sstevel@tonic-gate