untyped, unscoped, unchecked access to JVM objects;
authorwenzelm
Thu May 08 00:12:22 2014 +0200 (2014-05-08)
changeset 56905fb38a767a78b
parent 56902 f901a08c5653
child 56906 408b526911f7
untyped, unscoped, unchecked access to JVM objects;
src/Pure/General/untyped.scala
src/Pure/build-jars
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/Pure/General/untyped.scala	Thu May 08 00:12:22 2014 +0200
     1.3 @@ -0,0 +1,23 @@
     1.4 +/*  Title:      Pure/General/untyped.scala
     1.5 +    Module:     PIDE
     1.6 +    Author:     Makarius
     1.7 +
     1.8 +Untyped, unscoped, unchecked access to JVM objects.
     1.9 +*/
    1.10 +
    1.11 +package isabelle
    1.12 +
    1.13 +
    1.14 +object Untyped
    1.15 +{
    1.16 +  def get(obj: AnyRef, x: String): AnyRef =
    1.17 +  {
    1.18 +    obj.getClass.getDeclaredFields.find(_.getName == x) match {
    1.19 +      case Some(field) =>
    1.20 +        field.setAccessible(true)
    1.21 +        field.get(obj)
    1.22 +      case None => error("No field " + quote(x) + " for " + obj)
    1.23 +    }
    1.24 +  }
    1.25 +}
    1.26 +
     2.1 --- a/src/Pure/build-jars	Wed May 07 18:09:08 2014 +0200
     2.2 +++ b/src/Pure/build-jars	Thu May 08 00:12:22 2014 +0200
     2.3 @@ -37,6 +37,7 @@
     2.4    General/time.scala
     2.5    General/timing.scala
     2.6    General/url.scala
     2.7 +  General/untyped.scala
     2.8    General/word.scala
     2.9    General/xz_file.scala
    2.10    GUI/color_value.scala