1.1 --- a/src/Tools/jEdit/etc/options	Wed Sep 25 15:40:34 2013 +0200
     1.2 +++ b/src/Tools/jEdit/etc/options	Wed Sep 25 16:05:40 2013 +0200
     1.3 @@ -30,10 +30,10 @@
     1.4  public option jedit_symbols_search_limit : int = 50
     1.5    -- "maximum number of symbols in search result"
     1.6  
     1.7 -public option jedit_macos_application : bool = true
     1.8 +option jedit_macos_application : bool = false
     1.9    -- "some native Mac OS X application support (potential conflict with MacOSX plugin)"
    1.10  
    1.11 -public option jedit_macos_preferences : bool = false
    1.12 +option jedit_macos_preferences : bool = false
    1.13    -- "native Mac OS X preferences menu"
    1.14  
    1.15  public option jedit_timing_threshold : real = 0.1

     2.1 --- a/src/Tools/jEdit/src/plugin.scala	Wed Sep 25 15:40:34 2013 +0200
     2.2 +++ b/src/Tools/jEdit/src/plugin.scala	Wed Sep 25 16:05:40 2013 +0200
     2.3 @@ -325,7 +325,7 @@
     2.4        PIDE.options.update(Options.init())
     2.5        PIDE.completion_history.load()
     2.6  
     2.7 -      if (Platform.is_macos) OSX_Adapter.init
     2.8 +      // FIXME if (Platform.is_macos) OSX_Adapter.init
     2.9  
    2.10        SyntaxUtilities.setStyleExtender(new Token_Markup.Style_Extender)
    2.11        if (ModeProvider.instance.isInstanceOf[ModeProvider])