src/Pure/General/untyped.scala
changeset 56905 fb38a767a78b
child 58682 542fa5093ebf
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/General/untyped.scala	Thu May 08 00:12:22 2014 +0200
@@ -0,0 +1,23 @@
+/*  Title:      Pure/General/untyped.scala
+    Module:     PIDE
+    Author:     Makarius
+
+Untyped, unscoped, unchecked access to JVM objects.
+*/
+
+package isabelle
+
+
+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)
+    }
+  }
+}
+