more robust Mac OS X application support;

--- a/src/Tools/jEdit/etc/options	Mon Sep 09 15:53:02 2013 +0200
+++ b/src/Tools/jEdit/etc/options	Mon Sep 09 16:15:48 2013 +0200
@@ -27,8 +27,11 @@
 public option jedit_symbols_search_limit : int = 50
   -- "maximum number of symbols in search result"
 
-public option jedit_mac_adapter : bool = true
-  -- "some native Mac OS X support (potential conflict with MacOSX plugin)"
+public option jedit_macos_application : bool = true
+  -- "some native Mac OS X application support (potential conflict with MacOSX plugin)"
+
+public 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"

--- a/src/Tools/jEdit/src/osx_adapter.scala	Mon Sep 09 15:53:02 2013 +0200
+++ b/src/Tools/jEdit/src/osx_adapter.scala	Mon Sep 09 16:15:48 2013 +0200
@@ -9,26 +9,41 @@
 
 import isabelle._
 
-import java.lang.{Class, ClassNotFoundException}
+import java.lang.{Class, ClassNotFoundException, NoSuchMethodException}
 import java.lang.reflect.{InvocationHandler, Method, Proxy}
 
 
 object OSX_Adapter
 {
-  def set_quit_handler(target: AnyRef, quit_handler: Method)
+  private lazy val application_class: Class[_] = Class.forName("com.apple.eawt.Application")
+  private lazy val application = application_class.getConstructor().newInstance()
+
+  def init
   {
-    set_handler(new OSX_Adapter("handle_quit", target, quit_handler))
+    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")
+      }
+    }
   }
 
-  var application: Any = null
-
-  def set_handler(adapter: OSX_Adapter)
+  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_class: Class[_] = Class.forName("com.apple.eawt.Application")
-      if (application == null)
-        application = application_class.getConstructor().newInstance()
-
       val application_listener_class: Class[_] =
         Class.forName("com.apple.eawt.ApplicationListener")
       val add_listener_method =
@@ -58,9 +73,12 @@
 
       val event = args(0)
       if (event != null) {
-        val set_handled_method =
-          event.getClass.getDeclaredMethod("setHandled", classOf[java.lang.Boolean])
-        set_handled_method.invoke(event, java.lang.Boolean.valueOf(handled))
+        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

--- a/src/Tools/jEdit/src/plugin.scala	Mon Sep 09 15:53:02 2013 +0200
+++ b/src/Tools/jEdit/src/plugin.scala	Mon Sep 09 16:15:48 2013 +0200
@@ -14,6 +14,8 @@
 import scala.swing.{ListView, ScrollPane}
 
 import org.gjt.sp.jedit.{jEdit, EBMessage, EBPlugin, Buffer, View, Debug}
+import org.jedit.options.CombinedOptions
+import org.gjt.sp.jedit.gui.AboutDialog
 import org.gjt.sp.jedit.textarea.{JEditTextArea, TextArea}
 import org.gjt.sp.jedit.syntax.ModeProvider
 import org.gjt.sp.jedit.msg.{EditorStarted, BufferUpdate, EditPaneUpdate, PropertiesChanged}
@@ -222,12 +224,23 @@
 
   /* Mac OS X application hooks */
 
-  def handle_quit(): Boolean =
+  def handleQuit(): Boolean =
   {
     jEdit.exit(jEdit.getActiveView(), true)
     false
   }
 
+  def handlePreferences()
+  {
+    CombinedOptions.combinedOptions(jEdit.getActiveView())
+  }
+
+  def handleAbout(): Boolean =
+  {
+    new AboutDialog(jEdit.getActiveView())
+    true
+  }
+
 
   /* main plugin plumbing */
 
@@ -306,8 +319,7 @@
       PIDE.options.update(Options.init())
       PIDE.completion_history.load()
 
-      if (Platform.is_macos && PIDE.options.bool("jedit_mac_adapter"))
-        OSX_Adapter.set_quit_handler(this, this.getClass.getDeclaredMethod("handle_quit"))
+      if (Platform.is_macos) OSX_Adapter.init
 
       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
       if (ModeProvider.instance.isInstanceOf[ModeProvider])