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

     2.1 --- a/src/Tools/jEdit/lib/Tools/jedit	Mon Jan 28 23:56:13 2013 +0100
     2.2 +++ b/src/Tools/jEdit/lib/Tools/jedit	Thu Jan 31 22:21:05 2013 +0100
     2.3 @@ -27,6 +27,7 @@
     2.4    "src/jedit_options.scala"
     2.5    "src/jedit_thy_load.scala"
     2.6    "src/monitor_dockable.scala"
     2.7 +  "src/osx_adapter.scala"
     2.8    "src/output_dockable.scala"
     2.9    "src/plugin.scala"
    2.10    "src/pretty_text_area.scala"

     3.1 --- a/src/Tools/jEdit/src/isabelle_options.scala	Mon Jan 28 23:56:13 2013 +0100
     3.2 +++ b/src/Tools/jEdit/src/isabelle_options.scala	Thu Jan 31 22:21:05 2013 +0100
     3.3 @@ -43,9 +43,10 @@
     3.4    private val relevant_options =
     3.5      Set("jedit_logic", "jedit_font_scale", "jedit_symbols_search_limit", "jedit_text_overview_limit",
     3.6        "jedit_tooltip_bounds", "jedit_tooltip_font_scale", "jedit_tooltip_margin",
     3.7 -      "threads", "threads_trace", "parallel_proofs", "parallel_proofs_threshold",
     3.8 -      "editor_load_delay", "editor_input_delay", "editor_output_delay", "editor_reparse_limit",
     3.9 -      "editor_tracing_messages", "editor_update_delay", "editor_chart_delay")
    3.10 +      "jedit_mac_adapter", "threads", "threads_trace", "parallel_proofs",
    3.11 +      "parallel_proofs_threshold", "editor_load_delay", "editor_input_delay",
    3.12 +      "editor_output_delay", "editor_reparse_limit", "editor_tracing_messages",
    3.13 +      "editor_update_delay", "editor_chart_delay")
    3.14  
    3.15    relevant_options.foreach(PIDE.options.value.check_name _)
    3.16  

     4.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     4.2 +++ b/src/Tools/jEdit/src/osx_adapter.scala	Thu Jan 31 22:21:05 2013 +0100
     4.3 @@ -0,0 +1,69 @@
     4.4 +/*  Title:      Tools/jEdit/src/osx_adapter.scala
     4.5 +    Author:     Makarius
     4.6 +
     4.7 +Some native OS X support.
     4.8 +*/
     4.9 +
    4.10 +package isabelle.jedit
    4.11 +
    4.12 +
    4.13 +import isabelle._
    4.14 +
    4.15 +import java.lang.{Class, ClassNotFoundException}
    4.16 +import java.lang.reflect.{InvocationHandler, Method, Proxy}
    4.17 +
    4.18 +
    4.19 +object OSX_Adapter
    4.20 +{
    4.21 +  def set_quit_handler(target: AnyRef, quit_handler: Method)
    4.22 +  {
    4.23 +    set_handler(new OSX_Adapter("handle_quit", target, quit_handler))
    4.24 +  }
    4.25 +
    4.26 +  var application: Any = null
    4.27 +
    4.28 +  def set_handler(adapter: OSX_Adapter)
    4.29 +  {
    4.30 +    try {
    4.31 +      val application_class: Class[_] = Class.forName("com.apple.eawt.Application")
    4.32 +      if (application == null)
    4.33 +        application = application_class.getConstructor().newInstance()
    4.34 +
    4.35 +      val application_listener_class: Class[_] =
    4.36 +        Class.forName("com.apple.eawt.ApplicationListener")
    4.37 +      val add_listener_method =
    4.38 +        application_class.getDeclaredMethod("addApplicationListener", application_listener_class)
    4.39 +
    4.40 +      val osx_adapter_proxy =
    4.41 +        Proxy.newProxyInstance(classOf[OSX_Adapter].getClassLoader,
    4.42 +          Array(application_listener_class), adapter)
    4.43 +      add_listener_method.invoke(application, osx_adapter_proxy)
    4.44 +    }
    4.45 +    catch {
    4.46 +      case exn: ClassNotFoundException =>
    4.47 +        java.lang.System.err.println(
    4.48 +          "com.apple.eawt.Application unavailable -- cannot install native OS X handler")
    4.49 +    }
    4.50 +  }
    4.51 +}
    4.52 +
    4.53 +class OSX_Adapter(proxy_signature: String, target_object: AnyRef, target_method: Method)
    4.54 +  extends InvocationHandler
    4.55 +{
    4.56 +  override def invoke(proxy: Any, method: Method, args: Array[AnyRef]): AnyRef =
    4.57 +  {
    4.58 +    if (proxy_signature == method.getName && args.length == 1) {
    4.59 +      val result = target_method.invoke(target_object)
    4.60 +      val handled = result == null || result.toString == "true"
    4.61 +
    4.62 +      val event = args(0)
    4.63 +      if (event != null) {
    4.64 +        val set_handled_method =
    4.65 +          event.getClass.getDeclaredMethod("setHandled", classOf[java.lang.Boolean])
    4.66 +        set_handled_method.invoke(event, java.lang.Boolean.valueOf(handled))
    4.67 +      }
    4.68 +    }
    4.69 +    null
    4.70 +  }
    4.71 +}
    4.72 +

     5.1 --- a/src/Tools/jEdit/src/plugin.scala	Mon Jan 28 23:56:13 2013 +0100
     5.2 +++ b/src/Tools/jEdit/src/plugin.scala	Thu Jan 31 22:21:05 2013 +0100
     5.3 @@ -212,6 +212,15 @@
     5.4    }
     5.5  
     5.6  
     5.7 +  /* Mac OS X application hooks */
     5.8 +
     5.9 +  def handle_quit(): Boolean =
    5.10 +  {
    5.11 +    jEdit.exit(jEdit.getActiveView(), true)
    5.12 +    false
    5.13 +  }
    5.14 +
    5.15 +
    5.16    /* main plugin plumbing */
    5.17  
    5.18    override def handleMessage(message: EBMessage)
    5.19 @@ -280,6 +289,9 @@
    5.20        val init_options = Options.init()
    5.21        Swing_Thread.now { PIDE.options.update(init_options)  }
    5.22  
    5.23 +      if (Platform.is_macos && PIDE.options.bool("jedit_mac_adapter"))
    5.24 +        OSX_Adapter.set_quit_handler(this, this.getClass.getDeclaredMethod("handle_quit"))
    5.25 +
    5.26        SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
    5.27        if (ModeProvider.instance.isInstanceOf[ModeProvider])
    5.28          ModeProvider.instance = new Token_Markup.Mode_Provider(ModeProvider.instance)