# HG changeset patch
# User wenzelm
# Date 1380194906 -7200
# Node ID 48072f04983861bbb2cc776befe3026bbe1ae5f5
# Parent  5ff12177a067865b77ca0b6223543e462e67467f
obsolete (see also 48d13465c7c7);

diff -r 5ff12177a067 -r 48072f049838 src/Tools/jEdit/etc/options
--- a/src/Tools/jEdit/etc/options	Thu Sep 26 12:56:59 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Thu Sep 26 13:28:26 2013 +0200
@@ -30,12 +30,6 @@
 public option jedit_symbols_search_limit : int = 50
   -- "maximum number of symbols in search result"
 
-option jedit_macos_application : bool = false
-  -- "some native Mac OS X application support (potential conflict with MacOSX plugin)"
-
-option jedit_macos_preferences : bool = false
-  -- "native Mac OS X preferences menu"
-
 public option jedit_timing_threshold : real = 0.1
   -- "default threshold for timing display"
 
diff -r 5ff12177a067 -r 48072f049838 src/Tools/jEdit/lib/Tools/jedit
--- a/src/Tools/jEdit/lib/Tools/jedit	Thu Sep 26 12:56:59 2013 +0200
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Sep 26 13:28:26 2013 +0200
@@ -28,7 +28,6 @@
   "src/jedit_options.scala"
   "src/jedit_thy_load.scala"
   "src/monitor_dockable.scala"
-  "src/osx_adapter.scala"
   "src/output_dockable.scala"
   "src/plugin.scala"
   "src/pretty_text_area.scala"
diff -r 5ff12177a067 -r 48072f049838 src/Tools/jEdit/src/osx_adapter.scala
--- a/src/Tools/jEdit/src/osx_adapter.scala	Thu Sep 26 12:56:59 2013 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,87 +0,0 @@
-/*  Title:      Tools/jEdit/src/osx_adapter.scala
-    Author:     Makarius
-
-Some native OS X support.
-*/
-
-package isabelle.jedit
-
-
-import isabelle._
-
-import java.lang.{Class, ClassNotFoundException, NoSuchMethodException}
-import java.lang.reflect.{InvocationHandler, Method, Proxy}
-
-
-object OSX_Adapter
-{
-  private lazy val application_class: Class[_] = Class.forName("com.apple.eawt.Application")
-  private lazy val application = application_class.getConstructor().newInstance()
-
-  def init
-  {
-    if (PIDE.options.bool("jedit_macos_application")) {
-      try {
-        set_handler("handleQuit")
-        set_handler("handleAbout")
-
-        if (PIDE.options.bool("jedit_macos_preferences")) {
-          application_class.getDeclaredMethod("setEnabledPreferencesMenu", classOf[Boolean]).
-            invoke(application, java.lang.Boolean.valueOf(true))
-          set_handler("handlePreferences")
-        }
-      }
-      catch {
-        case exn: ClassNotFoundException =>
-          java.lang.System.err.println(
-            "com.apple.eawt.Application unavailable -- cannot install native OS X handler")
-      }
-    }
-  }
-
-  private def set_handler(name: String)
-  {
-    val handler = PIDE.plugin.getClass.getDeclaredMethod(name)
-    val adapter = new OSX_Adapter(name, PIDE.plugin, handler)
-    try {
-      val application_listener_class: Class[_] =
-        Class.forName("com.apple.eawt.ApplicationListener")
-      val add_listener_method =
-        application_class.getDeclaredMethod("addApplicationListener", application_listener_class)
-
-      val osx_adapter_proxy =
-        Proxy.newProxyInstance(classOf[OSX_Adapter].getClassLoader,
-          Array(application_listener_class), adapter)
-      add_listener_method.invoke(application, osx_adapter_proxy)
-    }
-    catch {
-      case exn: ClassNotFoundException =>
-        java.lang.System.err.println(
-          "com.apple.eawt.Application unavailable -- cannot install native OS X handler")
-    }
-  }
-}
-
-class OSX_Adapter(proxy_signature: String, target_object: AnyRef, target_method: Method)
-  extends InvocationHandler
-{
-  override def invoke(proxy: Any, method: Method, args: Array[AnyRef]): AnyRef =
-  {
-    if (proxy_signature == method.getName && args.length == 1) {
-      val result = target_method.invoke(target_object)
-      val handled = result == null || result.toString == "true"
-
-      val event = args(0)
-      if (event != null) {
-        try {
-          val set_handled_method =
-            event.getClass.getDeclaredMethod("setHandled", classOf[java.lang.Boolean])
-          set_handled_method.invoke(event, java.lang.Boolean.valueOf(handled))
-        }
-        catch { case _: NoSuchMethodException => }
-      }
-    }
-    null
-  }
-}
-
diff -r 5ff12177a067 -r 48072f049838 src/Tools/jEdit/src/plugin.scala
--- a/src/Tools/jEdit/src/plugin.scala	Thu Sep 26 12:56:59 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Sep 26 13:28:26 2013 +0200
@@ -325,8 +325,6 @@
       PIDE.options.update(Options.init())
       PIDE.completion_history.load()
 
-      // FIXME if (Platform.is_macos) OSX_Adapter.init
-
       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
       if (ModeProvider.instance.isInstanceOf[ModeProvider])
         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)