untyped, unscoped, unchecked access to JVM objects;

--- /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)
+    }
+  }
+}
+

--- a/src/Pure/build-jars	Wed May 07 18:09:08 2014 +0200
+++ b/src/Pure/build-jars	Thu May 08 00:12:22 2014 +0200
@@ -37,6 +37,7 @@
   General/time.scala
   General/timing.scala
   General/url.scala
+  General/untyped.scala
   General/word.scala
   General/xz_file.scala
   GUI/color_value.scala