src/Tools/jEdit/src/plugin.scala
changeset 51071 b7e7557e80b5
parent 50808 1702ed63c2db
child 51294 0850d43cb355
--- 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)