some native Mac OS X support, notably quit_handler (important for dialog on unsaved changes);

--- a/src/Tools/jEdit/etc/options	Mon Jan 28 23:56:13 2013 +0100
+++ b/src/Tools/jEdit/etc/options	Thu Jan 31 22:21:05 2013 +0100
@@ -21,6 +21,9 @@
 option jedit_symbols_search_limit : int = 50
   -- "maximum number of symbols in search result"
 
+option jedit_mac_adapter : bool = true
+  -- "some native Mac OS X support (potential conflict with MacOSX plugin)"
+
 
 section "Rendering of Document Content"
 

--- a/src/Tools/jEdit/lib/Tools/jedit	Mon Jan 28 23:56:13 2013 +0100
+++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Jan 31 22:21:05 2013 +0100
@@ -27,6 +27,7 @@
   "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"

--- a/src/Tools/jEdit/src/isabelle_options.scala	Mon Jan 28 23:56:13 2013 +0100
+++ b/src/Tools/jEdit/src/isabelle_options.scala	Thu Jan 31 22:21:05 2013 +0100
@@ -43,9 +43,10 @@
   private val relevant_options =
     Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit",
       "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
-      "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold",
-      "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
-      "editor_tracing_messages", "editor_update_delay", "editor_chart_delay")
+      "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
+      "parallel_proofs_threshold", "editor_load_delay", "editor_input_delay",
+      "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
+      "editor_update_delay", "editor_chart_delay")
 
   relevant_options.foreach(PIDE.options.value.check_name _)
 

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/src/osx_adapter.scala	Thu Jan 31 22:21:05 2013 +0100
@@ -0,0 +1,69 @@
+/*  Title:      Tools/jEdit/src/osx_adapter.scala
+    Author:     Makarius
+
+Some native OS X support.
+*/
+
+package isabelle.jedit
+
+
+import isabelle._
+
+import java.lang.{Class, ClassNotFoundException}
+import java.lang.reflect.{InvocationHandler, Method, Proxy}
+
+
+object OSX_Adapter
+{
+  def set_quit_handler(target: AnyRef, quit_handler: Method)
+  {
+    set_handler(new OSX_Adapter("handle_quit", target, quit_handler))
+  }
+
+  var application: Any = null
+
+  def set_handler(adapter: OSX_Adapter)
+  {
+    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 =
+        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) {
+        val set_handled_method =
+          event.getClass.getDeclaredMethod("setHandled", classOf[java.lang.Boolean])
+        set_handled_method.invoke(event, java.lang.Boolean.valueOf(handled))
+      }
+    }
+    null
+  }
+}
+

--- a/src/Tools/jEdit/src/plugin.scala	Mon Jan 28 23:56:13 2013 +0100
+++ b/src/Tools/jEdit/src/plugin.scala	Thu Jan 31 22:21:05 2013 +0100
@@ -212,6 +212,15 @@
   }
 
 
+  /* Mac OS X application hooks */
+
+  def handle_quit(): Boolean =
+  {
+    jEdit.exit(jEdit.getActiveView(), true)
+    false
+  }
+
+
   /* main plugin plumbing */
 
   override def handleMessage(message: EBMessage)
@@ -280,6 +289,9 @@
       val init_options = Options.init()
       Swing_Thread.now { PIDE.options.update(init_options)  }
 
+      if (Platform.is_macos && PIDE.options.bool("jedit_mac_adapter"))
+        OSX_Adapter.set_quit_handler(this, this.getClass.getDeclaredMethod("handle_quit"))
+
       SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
       if (ModeProvider.instance.isInstanceOf[ModeProvider])
         ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)