# HG changeset patch
# User wenzelm
# Date 1467884778 -7200
# Node ID f473b6b16c635638bd19db1f8d29083c9e6aa353
# Parent  3f3223b90239a1d2d801ce973e34c947cb757aea
more operations;

diff -r 3f3223b90239 -r f473b6b16c63 src/Pure/General/untyped.scala
--- a/src/Pure/General/untyped.scala	Thu Jul 07 09:24:03 2016 +0200
+++ b/src/Pure/General/untyped.scala	Thu Jul 07 11:46:18 2016 +0200
@@ -8,7 +8,7 @@
 package isabelle
 
 
-import java.lang.reflect.Method
+import java.lang.reflect.{Method, Field}
 
 
 object Untyped
@@ -30,20 +30,25 @@
     }
   }
 
+  def field(obj: AnyRef, x: String): Field =
+  {
+    val iterator =
+      for {
+        c <- classes(obj)
+        field <- c.getDeclaredFields.iterator
+        if field.getName == x
+      } yield {
+        field.setAccessible(true)
+        field
+      }
+    if (iterator.hasNext) iterator.next
+    else error("No field " + quote(x) + " for " + obj)
+  }
+
   def get[A](obj: AnyRef, x: String): A =
     if (obj == null) null.asInstanceOf[A]
-    else {
-      val iterator =
-        for {
-          c <- classes(obj)
-          field <- c.getDeclaredFields.iterator
-          if field.getName == x
-        } yield {
-          field.setAccessible(true)
-          field.get(obj)
-        }
-      if (iterator.hasNext) iterator.next.asInstanceOf[A]
-      else error("No field " + quote(x) + " for " + obj)
-    }
+    else field(obj, x).get(obj).asInstanceOf[A]
+
+  def set[A](obj: AnyRef, x: String, y: A): Unit =
+    field(obj, x).set(obj, y)
 }
-