📄 globaloptions.java
字号:
/* * GlobalOptions.java - Global options dialog * :tabSize=8:indentSize=8:noTabs=false: * :folding=explicit:collapseFolds=1: * * Copyright (C) 2002 Slava Pestov * * This program is free software; you can redistribute it and/or * modify it under the terms of the GNU General Public License * as published by the Free Software Foundation; either version 2 * of the License, or any later version. * * This program is distributed in the hope that it will be useful, * but WITHOUT ANY WARRANTY; without even the implied warranty of * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the * GNU General Public License for more details. * * You should have received a copy of the GNU General Public License * along with this program; if not, write to the Free Software * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. */package org.gjt.sp.jedit.options;//{{{ Importsimport java.awt.Dialog;import java.awt.Frame;import org.gjt.sp.jedit.gui.OptionsDialog;import org.gjt.sp.jedit.options.*;import org.gjt.sp.jedit.*;import org.gjt.sp.util.Log;//}}}public class GlobalOptions extends OptionsDialog{ //{{{ GlobalOptions constructor public GlobalOptions(Frame frame) { super(frame,"options",jEdit.getProperty("options.last")); } //}}} //{{{ GlobalOptions constructor public GlobalOptions(Frame frame, String pane) { super(frame,"options",pane); } //}}} //{{{ GlobalOptions constructor public GlobalOptions(Dialog dialog) { super(dialog,"options",jEdit.getProperty("options.last")); } //}}} //{{{ GlobalOptions constructor public GlobalOptions(Dialog dialog, String pane) { super(dialog,"options",pane); } //}}} //{{{ createOptionTreeModel() method protected OptionTreeModel createOptionTreeModel() { OptionTreeModel paneTreeModel = new OptionTreeModel(); OptionGroup rootGroup = (OptionGroup) paneTreeModel.getRoot(); // initialize the jEdit branch of the options tree jEditGroup = new OptionGroup("jedit"); addOptionPane(new AbbrevsOptionPane(), jEditGroup); addOptionPane(new AppearanceOptionPane(), jEditGroup); addOptionPane(new ContextOptionPane(), jEditGroup); addOptionPane(new DockingOptionPane(), jEditGroup); addOptionPane(new EditingOptionPane(), jEditGroup); addOptionPane(new GeneralOptionPane(), jEditGroup); addOptionPane(new GutterOptionPane(), jEditGroup); addOptionPane(new LoadSaveOptionPane(), jEditGroup); addOptionPane(new PrintOptionPane(), jEditGroup); addOptionPane(new FirewallOptionPane(), jEditGroup); addOptionPane(new ShortcutsOptionPane(), jEditGroup); addOptionPane(new StatusBarOptionPane(), jEditGroup); addOptionPane(new SyntaxHiliteOptionPane(), jEditGroup); addOptionPane(new TextAreaOptionPane(), jEditGroup); addOptionPane(new ToolBarOptionPane(), jEditGroup); addOptionGroup(jEditGroup, rootGroup); browserGroup = new OptionGroup("browser"); addOptionPane(new BrowserColorsOptionPane(), browserGroup); addOptionPane(new BrowserOptionPane(), browserGroup); addOptionGroup(browserGroup, rootGroup); // initialize the Plugins branch of the options tree pluginsGroup = new OptionGroup("plugins"); // Query plugins for option panes EditPlugin[] plugins = jEdit.getPlugins(); for(int i = 0; i < plugins.length; i++) { EditPlugin ep = plugins[i]; try { ep.createOptionPanes(this); } catch(Throwable t) { Log.log(Log.ERROR, ep, "Error creating option pane"); Log.log(Log.ERROR, ep, t); } } // only add the Plugins branch if there are OptionPanes if (pluginsGroup.getMemberCount() > 0) { addOptionGroup(pluginsGroup, rootGroup); } return paneTreeModel; } //}}} //{{{ getDefaultGroup() method protected OptionGroup getDefaultGroup() { return pluginsGroup; } //}}} //{{{ Private members private OptionGroup jEditGroup; private OptionGroup browserGroup; private OptionGroup pluginsGroup; //}}}}
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -