--- 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)