added Untyped.method convenience (for *this* class only);
authorwenzelm
Tue Dec 02 17:30:53 2014 +0100 (2014-12-02)
changeset 59080611914621edb
parent 59079 12a689755c3d
child 59081 2ceb05ee0331
added Untyped.method convenience (for *this* class only);
src/Pure/GUI/gui.scala
src/Pure/General/untyped.scala
src/Pure/Tools/main.scala
src/Tools/jEdit/src/document_model.scala
src/Tools/jEdit/src/jedit_editor.scala
src/Tools/jEdit/src/spell_checker.scala
     1.1 --- a/src/Pure/GUI/gui.scala	Tue Dec 02 16:40:11 2014 +0100
     1.2 +++ b/src/Pure/GUI/gui.scala	Tue Dec 02 17:30:53 2014 +0100
     1.3 @@ -60,13 +60,11 @@
     1.4      if (Platform.is_windows || Platform.is_macos) None
     1.5      else
     1.6        try {
     1.7 -        val XWM = Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader)
     1.8 -        val getWM = XWM.getDeclaredMethod("getWM")
     1.9 -        getWM.setAccessible(true)
    1.10 -        getWM.invoke(null) match {
    1.11 -          case null => None
    1.12 -          case wm => Some(wm.toString)
    1.13 -        }
    1.14 +        val wm =
    1.15 +          Untyped.method(Class.forName("sun.awt.X11.XWM", true, ClassLoader.getSystemClassLoader),
    1.16 +            "getWM").invoke(null)
    1.17 +        if (wm == null) None
    1.18 +        else Some(wm.toString)
    1.19        }
    1.20        catch {
    1.21          case _: ClassNotFoundException => None
     2.1 --- a/src/Pure/General/untyped.scala	Tue Dec 02 16:40:11 2014 +0100
     2.2 +++ b/src/Pure/General/untyped.scala	Tue Dec 02 17:30:53 2014 +0100
     2.3 @@ -8,8 +8,18 @@
     2.4  package isabelle
     2.5  
     2.6  
     2.7 +import java.lang.reflect.Method
     2.8 +
     2.9 +
    2.10  object Untyped
    2.11  {
    2.12 +  def method(c: Class[_], name: String, arg_types: Class[_]*): Method =
    2.13 +  {
    2.14 +    val m = c.getDeclaredMethod(name, arg_types: _*)
    2.15 +    m.setAccessible(true)
    2.16 +    m
    2.17 +  }
    2.18 +
    2.19    def classes(obj: AnyRef): Iterator[Class[_ <: AnyRef]] = new Iterator[Class[_ <: AnyRef]] {
    2.20      private var next_elem: Class[_ <: AnyRef] = obj.getClass
    2.21      def hasNext(): Boolean = next_elem != null
     3.1 --- a/src/Pure/Tools/main.scala	Tue Dec 02 16:40:11 2014 +0100
     3.2 +++ b/src/Pure/Tools/main.scala	Tue Dec 02 17:30:53 2014 +0100
     3.3 @@ -122,7 +122,7 @@
     3.4  
     3.5            val jedit =
     3.6              Class.forName("org.gjt.sp.jedit.jEdit", true, ClassLoader.getSystemClassLoader)
     3.7 -          val jedit_main = jedit.getDeclaredMethod("main", classOf[Array[String]])
     3.8 +          val jedit_main = jedit.getMethod("main", classOf[Array[String]])
     3.9  
    3.10            () => jedit_main.invoke(null, jedit_options ++ jedit_settings ++ more_args)
    3.11          }
     4.1 --- a/src/Tools/jEdit/src/document_model.scala	Tue Dec 02 16:40:11 2014 +0100
     4.2 +++ b/src/Tools/jEdit/src/document_model.scala	Tue Dec 02 17:30:53 2014 +0100
     4.3 @@ -289,12 +289,9 @@
     4.4    def syntax_changed()
     4.5    {
     4.6      Untyped.get[LineManager](buffer, "lineMgr").setFirstInvalidLineContext(0)
     4.7 -    for (text_area <- JEdit_Lib.jedit_text_areas(buffer)) {
     4.8 -      val c = Class.forName("org.gjt.sp.jedit.textarea.TextArea")
     4.9 -      val m = c.getDeclaredMethod("foldStructureChanged")
    4.10 -      m.setAccessible(true)
    4.11 -      m.invoke(text_area)
    4.12 -    }
    4.13 +    for (text_area <- JEdit_Lib.jedit_text_areas(buffer))
    4.14 +      Untyped.method(Class.forName("org.gjt.sp.jedit.textarea.TextArea"), "foldStructureChanged").
    4.15 +        invoke(text_area)
    4.16    }
    4.17  
    4.18    private def init_token_marker()
     5.1 --- a/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 02 16:40:11 2014 +0100
     5.2 +++ b/src/Tools/jEdit/src/jedit_editor.scala	Tue Dec 02 17:30:53 2014 +0100
     5.3 @@ -128,10 +128,7 @@
     5.4    {
     5.5      val navigator = jEdit.getPlugin("ise.plugin.nav.NavigatorPlugin")
     5.6      if (navigator != null) {
     5.7 -      try {
     5.8 -        val m = navigator.getClass.getDeclaredMethod("pushPosition", view.getClass)
     5.9 -        m.invoke(null, view)
    5.10 -      }
    5.11 +      try { Untyped.method(navigator.getClass, "pushPosition", view.getClass).invoke(null, view) }
    5.12        catch { case _: NoSuchMethodException => }
    5.13      }
    5.14    }
     6.1 --- a/src/Tools/jEdit/src/spell_checker.scala	Tue Dec 02 16:40:11 2014 +0100
     6.2 +++ b/src/Tools/jEdit/src/spell_checker.scala	Tue Dec 02 17:30:53 2014 +0100
     6.3 @@ -255,17 +255,14 @@
     6.4      factory_cons.setAccessible(true)
     6.5      val factory = factory_cons.newInstance()
     6.6  
     6.7 -    val add = factory_class.getDeclaredMethod("add", classOf[String])
     6.8 -    add.setAccessible(true)
     6.9 +    val add = Untyped.method(factory_class, "add", classOf[String])
    6.10  
    6.11      for {
    6.12        word <- main_dictionary.iterator ++ included_iterator()
    6.13        if !excluded(word)
    6.14      } add.invoke(factory, word)
    6.15  
    6.16 -    val create = factory_class.getDeclaredMethod("create")
    6.17 -    create.setAccessible(true)
    6.18 -    dict = create.invoke(factory)
    6.19 +    dict = Untyped.method(factory_class, "create").invoke(factory)
    6.20    }
    6.21    load()
    6.22  
    6.23 @@ -299,10 +296,7 @@
    6.24  
    6.25      if (include) {
    6.26        if (permanent) save()
    6.27 -
    6.28 -      val m = dict.getClass.getDeclaredMethod("add", classOf[String])
    6.29 -      m.setAccessible(true)
    6.30 -      m.invoke(dict, word)
    6.31 +      Untyped.method(dict.getClass, "add", classOf[String]).invoke(dict, word)
    6.32      }
    6.33      else { save(); load() }
    6.34    }
    6.35 @@ -320,11 +314,8 @@
    6.36    /* check known words */
    6.37  
    6.38    def contains(word: String): Boolean =
    6.39 -  {
    6.40 -    val m = dict.getClass.getSuperclass.getDeclaredMethod("exist", classOf[String])
    6.41 -    m.setAccessible(true)
    6.42 -    m.invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
    6.43 -  }
    6.44 +    Untyped.method(dict.getClass.getSuperclass, "exist", classOf[String]).
    6.45 +      invoke(dict, word).asInstanceOf[java.lang.Boolean].booleanValue
    6.46  
    6.47    def check(word: String): Boolean =
    6.48      word match {
    6.49 @@ -342,10 +333,9 @@
    6.50  
    6.51    private def suggestions(word: String): Option[List[String]] =
    6.52    {
    6.53 -    val m = dict.getClass.getSuperclass.getDeclaredMethod("searchSuggestions", classOf[String])
    6.54 -    m.setAccessible(true)
    6.55      val res =
    6.56 -      m.invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
    6.57 +      Untyped.method(dict.getClass.getSuperclass, "searchSuggestions", classOf[String]).
    6.58 +        invoke(dict, word).asInstanceOf[java.util.List[AnyRef]].toArray.toList.map(_.toString)
    6.59      if (res.isEmpty) None else Some(res)
    6.60    }
    6.61