# HG changeset patch
# User wenzelm
# Date 1399500742 -7200
# Node ID fb38a767a78b130be9b965d898b830ac825fce5b
# Parent  f901a08c5653c05c4ae18195079343f6df63aff0
untyped, unscoped, unchecked access to JVM objects;

diff -r f901a08c5653 -r fb38a767a78b src/Pure/General/untyped.scala
--- /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)
+    }
+  }
+}
+
diff -r f901a08c5653 -r fb38a767a78b src/Pure/build-jars
--- 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