src/Pure/General/untyped.scala
author wenzelm
Thu, 08 May 2014 00:12:22 +0200
changeset 56905 fb38a767a78b
child 58682 542fa5093ebf
permissions -rw-r--r--
untyped, unscoped, unchecked access to JVM objects;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
56905
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/General/untyped.scala
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
     2
    Module:     PIDE
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
     3
    Author:     Makarius
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
     4
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
     5
Untyped, unscoped, unchecked access to JVM objects.
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
     6
*/
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
     7
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
     8
package isabelle
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
     9
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    10
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    11
object Untyped
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    12
{
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    13
  def get(obj: AnyRef, x: String): AnyRef =
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    14
  {
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    15
    obj.getClass.getDeclaredFields.find(_.getName == x) match {
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    16
      case Some(field) =>
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    17
        field.setAccessible(true)
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    18
        field.get(obj)
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    19
      case None => error("No field " + quote(x) + " for " + obj)
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    20
    }
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    21
  }
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    22
}
fb38a767a78b untyped, unscoped, unchecked access to JVM objects;
wenzelm
parents:
diff changeset
    23