added Untyped.method convenience (for *this* class only);

--- a/src/Pure/GUI/gui.scala	Tue Dec 02 16:40:11 2014 +0100
+++ b/src/Pure/GUI/gui.scala	Tue Dec 02 17:30:53 2014 +0100
@@ -60,13 +60,11 @@
     if (Platform.is_windows || Platform.is_macos) None
     else
       try {
-        val XWM = Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader)
-        val getWM = XWM.getDeclaredMethod("getWM")
-        getWM.setAccessible(true)
-        getWM.invoke(null) match {
-          case null => None
-          case wm => Some(wm.toString)
-        }
+        val wm =
+          Untyped.method(Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader),
+            "getWM").invoke(null)
+        if (wm == null) None
+        else Some(wm.toString)
       }
       catch {
         case _: ClassNotFoundException => None

--- a/src/Pure/General/untyped.scala	Tue Dec 02 16:40:11 2014 +0100
+++ b/src/Pure/General/untyped.scala	Tue Dec 02 17:30:53 2014 +0100
@@ -8,8 +8,18 @@
 package isabelle
 
 
+import java.lang.reflect.Method
+
+
 object Untyped
 {
+  def method(c: Class[_], name: String, arg_types: Class[_]*): Method =
+  {
+    val m = c.getDeclaredMethod(name, arg_types: _*)
+    m.setAccessible(true)
+    m
+  }
+
   def classes(obj: AnyRef): Iterator[Class[_ <: AnyRef]] = new Iterator[Class[_ <: AnyRef]] {
     private var next_elem: Class[_ <: AnyRef] = obj.getClass
     def hasNext(): Boolean = next_elem != null

--- a/src/Pure/Tools/main.scala	Tue Dec 02 16:40:11 2014 +0100
+++ b/src/Pure/Tools/main.scala	Tue Dec 02 17:30:53 2014 +0100
@@ -122,7 +122,7 @@
 
           val jedit =
             Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
-          val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]])
+          val jedit_main = jedit.getMethod("main", classOf[Array[String]])
 
           () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
         }

--- a/src/Tools/jEdit/src/document_model.scala	Tue Dec 02 16:40:11 2014 +0100
+++ b/src/Tools/jEdit/src/document_model.scala	Tue Dec 02 17:30:53 2014 +0100
@@ -289,12 +289,9 @@
   def syntax_changed()
   {
     Untyped.get[LineManager](buffer, "lineMgr").setFirstInvalidLineContext(0)
-    for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
-      val c = Class.forName("org.gjt.sp.jedit.textarea.TextArea")
-      val m = c.getDeclaredMethod("foldStructureChanged")
-      m.setAccessible(true)
-      m.invoke(text_area)
-    }
+    for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
+      Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
+        invoke(text_area)
   }
 
   private def init_token_marker()

--- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 02 16:40:11 2014 +0100
+++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 02 17:30:53 2014 +0100
@@ -128,10 +128,7 @@
   {
     val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
     if (navigator != null) {
-      try {
-        val m = navigator.getClass.getDeclaredMethod("pushPosition", view.getClass)
-        m.invoke(null, view)
-      }
+      try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
       catch { case _: NoSuchMethodException => }
     }
   }

--- a/src/Tools/jEdit/src/spell_checker.scala	Tue Dec 02 16:40:11 2014 +0100
+++ b/src/Tools/jEdit/src/spell_checker.scala	Tue Dec 02 17:30:53 2014 +0100
@@ -255,17 +255,14 @@
     factory_cons.setAccessible(true)
     val factory = factory_cons.newInstance()
 
-    val add = factory_class.getDeclaredMethod("add", classOf[String])
-    add.setAccessible(true)
+    val add = Untyped.method(factory_class, "add", classOf[String])
 
     for {
       word <- main_dictionary.iterator ++ included_iterator()
       if !excluded(word)
     } add.invoke(factory, word)
 
-    val create = factory_class.getDeclaredMethod("create")
-    create.setAccessible(true)
-    dict = create.invoke(factory)
+    dict = Untyped.method(factory_class, "create").invoke(factory)
   }
   load()
 
@@ -299,10 +296,7 @@
 
     if (include) {
       if (permanent) save()
-
-      val m = dict.getClass.getDeclaredMethod("add", classOf[String])
-      m.setAccessible(true)
-      m.invoke(dict, word)
+      Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word)
     }
     else { save(); load() }
   }
@@ -320,11 +314,8 @@
   /* check known words */
 
   def contains(word: String): Boolean =
-  {
-    val m = dict.getClass.getSuperclass.getDeclaredMethod("exist", classOf[String])
-    m.setAccessible(true)
-    m.invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
-  }
+    Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]).
+      invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
 
   def check(word: String): Boolean =
     word match {
@@ -342,10 +333,9 @@
 
   private def suggestions(word: String): Option[List[String]] =
   {
-    val m = dict.getClass.getSuperclass.getDeclaredMethod("searchSuggestions", classOf[String])
-    m.setAccessible(true)
     val res =
-      m.invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
+      Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
+        invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
     if (res.isEmpty) None else Some(res)
   }