📄 panelwindowcontainer.java
字号:
/* * PanelWindowContainer.java - holds dockable windows * :tabSize=8:indentSize=8:noTabs=false: * :folding=explicit:collapseFolds=1: * * Copyright (C) 2000, 2001, 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.gui;//{{{ Importsimport javax.swing.border.*;import javax.swing.plaf.metal.*;import javax.swing.*;import java.awt.event.*;import java.awt.font.*;import java.awt.geom.AffineTransform;import java.awt.*;import java.util.Vector;import org.gjt.sp.jedit.*;//}}}/** * A container for dockable windows. This class should never be used * directly. * @author Slava Pestov * @version $Id: PanelWindowContainer.java,v 1.49 2003/02/05 00:40:22 spestov Exp $ * @since jEdit 4.0pre1 */public class PanelWindowContainer implements DockableWindowContainer{ //{{{ PanelWindowContainer constructor public PanelWindowContainer(DockableWindowManager wm, String position) { this.wm = wm; this.position = position; //{{{ Button box setup buttons = new JPanel(new ButtonLayout()); buttons.setBorder(new EmptyBorder(1,1,1,1)); // the close box must be the same size as the other buttons to look good. // there are two ways to achieve this: // a) write a custom layout manager // b) when the first button is added, give the close box the proper size // I'm lazy so I chose "b". See register() for details. closeBox = new JButton(GUIUtilities.loadIcon("closebox.gif")); closeBox.setRequestFocusEnabled(false); closeBox.setToolTipText(jEdit.getProperty("view.docking.close-tooltip")); if(OperatingSystem.isMacOSLF()) closeBox.putClientProperty("JButton.buttonType","toolbar"); // makes it look a bit better int left; if(position.equals(DockableWindowManager.RIGHT) || position.equals(DockableWindowManager.LEFT)) left = 1; else left = 0; closeBox.setMargin(new Insets(0,left,0,0)); buttons.add(closeBox); closeBox.addActionListener(new ActionHandler()); closeBox.addMouseListener(new MouseHandler()); popupButton = new JButton(GUIUtilities.loadIcon("ToolbarMenu.gif")); popupButton.setRequestFocusEnabled(false); popupButton.setToolTipText(jEdit.getProperty("view.docking.menu-tooltip")); if(OperatingSystem.isMacOSLF()) popupButton.putClientProperty("JButton.buttonType","toolbar"); buttons.add(popupButton); popupButton.addMouseListener(new MouseHandler()); buttonGroup = new ButtonGroup(); // JDK 1.4 workaround buttonGroup.add(nullButton = new JToggleButton()); //}}} dockables = new Vector(); dockablePanel = new DockablePanel(); dimension = jEdit.getIntegerProperty( "view.dock." + position + ".dimension",0); buttons.addMouseListener(new MouseHandler()); } //}}} //{{{ register() method public void register(final DockableWindowManager.Entry entry) { dockables.addElement(entry); //{{{ Create button int rotation; if(position.equals(DockableWindowManager.TOP) || position.equals(DockableWindowManager.BOTTOM)) rotation = RotatedTextIcon.NONE; else if(position.equals(DockableWindowManager.LEFT)) rotation = RotatedTextIcon.CCW; else if(position.equals(DockableWindowManager.RIGHT)) rotation = RotatedTextIcon.CW; else throw new InternalError("Invalid position: " + position); JToggleButton button = new JToggleButton(); button.setMargin(new Insets(0,0,0,0)); button.setRequestFocusEnabled(false); button.setIcon(new RotatedTextIcon(rotation,button.getFont(), entry.title)); button.setActionCommand(entry.factory.name); button.addActionListener(new ActionHandler()); if(OperatingSystem.isMacOSLF()) button.putClientProperty("JButton.buttonType","toolbar"); //}}} buttonGroup.add(button); buttons.add(button); button.addMouseListener(new MouseHandler()); wm.revalidate(); } //}}} //{{{ add() method public void add(DockableWindowManager.Entry entry) { dockablePanel.add(entry.factory.name,entry.win); } //}}} //{{{ remove() method public void remove(DockableWindowManager.Entry entry) { if(entry.factory.name.equals(mostRecent)) mostRecent = null; int index = dockables.indexOf(entry); buttons.remove(index + 2); dockables.removeElement(entry); if(entry.win != null) dockablePanel.remove(entry.win); if(current == entry) { current = null; show(null); } else wm.revalidate(); } //}}} //{{{ save() method public void save(DockableWindowManager.Entry entry) {} //}}} //{{{ showMostRecent() method public void showMostRecent() { if(dockables.size() == 0) { Toolkit.getDefaultToolkit().beep(); return; } if(mostRecent == null) { mostRecent = ((DockableWindowManager.Entry) dockables.get(0)).factory.name; } wm.showDockableWindow(mostRecent); } //}}} //{{{ show() method public void show(final DockableWindowManager.Entry entry) { if(current == entry) { if(entry != null) { entry.win.requestFocus(); entry.win.requestDefaultFocus(); } return; } if(current == null) { // we didn't have a component previously, so create a border dockablePanel.setBorder(new DockBorder(position)); } if(entry != null) { mostRecent = entry.factory.name; this.current = entry; dockablePanel.showDockable(entry.factory.name); int index = dockables.indexOf(entry); ((JToggleButton)buttons.getComponent(index + 2)).setSelected(true); entry.win.requestFocus(); entry.win.requestDefaultFocus(); } else { current = null; nullButton.setSelected(true); // removing last component, so remove border dockablePanel.setBorder(null); wm.getView().getTextArea().requestFocus(); } wm.revalidate(); dockablePanel.repaint(); } //}}} //{{{ isVisible() method public boolean isVisible(DockableWindowManager.Entry entry) { return current == entry; } //}}} //{{{ getCurrent() method public DockableWindowManager.Entry getCurrent() { return current; } //}}} //{{{ getDockables() method public String[] getDockables() { String[] retVal = new String[dockables.size()]; for(int i = 0; i < dockables.size(); i++) { DockableWindowManager.Entry entry = (DockableWindowManager.Entry) dockables.elementAt(i); retVal[i] = entry.factory.name; } return retVal; } //}}} //{{{ Package-private members static final int SPLITTER_WIDTH = 10; DockablePanel dockablePanel; //{{{ save() method void save() { jEdit.setIntegerProperty("view.dock." + position + ".dimension", dimension); if(current == null) jEdit.unsetProperty("view.dock." + position + ".last"); else { jEdit.setProperty("view.dock." + position + ".last", current.factory.name); } } //}}} //{{{ getButtonBox() method JPanel getButtonBox() { return buttons; } //}}} //{{{ getDockablePanel() method DockablePanel getDockablePanel() { return dockablePanel; } //}}} //{{{ setDimension() method void setDimension(int dimension) { if(dimension != 0) this.dimension = dimension - SPLITTER_WIDTH - 3; } //}}} //}}} //{{{ Private members private DockableWindowManager wm; private String position; private JPanel buttons; private JButton closeBox; private JButton popupButton; private ButtonGroup buttonGroup; private JToggleButton nullButton; private int dimension; private Vector dockables; private DockableWindowManager.Entry current; // remember the most recent dockable private String mostRecent; //}}} //{{{ Inner classes //{{{ ActionHandler class class ActionHandler implements ActionListener { public void actionPerformed(ActionEvent evt) { if(evt.getSource() == closeBox) show(null); else { if(wm.isDockableWindowVisible(evt.getActionCommand())) show(null); else wm.showDockableWindow(evt.getActionCommand()); } } } //}}} //{{{ MouseHandler class class MouseHandler extends MouseAdapter { JPopupMenu popup; public void mousePressed(MouseEvent evt) { if(evt.getSource() == popupButton || GUIUtilities.isPopupTrigger(evt)) { if(popup != null && popup.isVisible()) popup.setVisible(false); else { popup = createPopupMenu(); GUIUtilities.showPopupMenu(popup, (Component)evt.getSource(), evt.getX(),evt.getY()); } } } private JPopupMenu createPopupMenu() { JPopupMenu popup = new JPopupMenu(); JMenu floatMenu = new JMenu(jEdit.getProperty("view.docking.menu-float")); String[] dockables = getDockables(); for(int i = 0; i < dockables.length; i++) { final String entry = dockables[i]; JMenuItem selectMenuItem = new JMenuItem(wm.getDockableTitle(entry)); selectMenuItem.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent evt) { wm.showDockableWindow(entry); } }); JMenuItem floatMenuItem = new JMenuItem(wm.getDockableTitle(entry)); floatMenuItem.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent evt) { wm.floatDockableWindow(entry); } }); popup.add(selectMenuItem); floatMenu.add(floatMenuItem); } popup.addSeparator(); popup.add(floatMenu); popup.addSeparator(); JMenuItem config = new JMenuItem(jEdit.getProperty("view.docking.menu-config")); config.addActionListener(new ActionListener() { public void actionPerformed(ActionEvent evt) { new org.gjt.sp.jedit.options.GlobalOptions( wm.getView(),"docking"); } }); popup.add(config); return popup; } } //}}} //{{{ DockBorder class static class DockBorder implements Border { String position; Insets insets; Color color1; Color color2; Color color3; //{{{ DockBorder constructor DockBorder(String position) { this.position = position; insets = new Insets( position.equals(DockableWindowManager.BOTTOM) ? SPLITTER_WIDTH : 0, position.equals(DockableWindowManager.RIGHT) ? SPLITTER_WIDTH : 0, position.equals(DockableWindowManager.TOP) ? SPLITTER_WIDTH : 0, position.equals(DockableWindowManager.LEFT) ? SPLITTER_WIDTH : 0); } //}}} //{{{ paintBorder() method public void paintBorder(Component c, Graphics g, int x, int y, int width, int height) { updateColors(); if(color1 == null || color2 == null || color3 == null) return; if(position.equals(DockableWindowManager.BOTTOM)) paintHorizBorder(g,x,y,width); else if(position.equals(DockableWindowManager.RIGHT)) paintVertBorder(g,x,y,height); else if(position.equals(DockableWindowManager.TOP)) { paintHorizBorder(g,x,y + height - SPLITTER_WIDTH,width); } else if(position.equals(DockableWindowManager.LEFT)) { paintVertBorder(g,x + width - SPLITTER_WIDTH,y,height); } } //}}} //{{{ getBorderInsets() method public Insets getBorderInsets(Component c) { return insets; } //}}} //{{{ isBorderOpaque() method public boolean isBorderOpaque() { return false; } //}}} //{{{ paintHorizBorder() method private void paintHorizBorder(Graphics g, int x, int y, int width) { g.setColor(color3); g.fillRect(x,y,width,SPLITTER_WIDTH); for(int i = 0; i < width / 4 - 1; i++)
⌨️ 快捷键说明
复制代码
Ctrl + C
搜索代码
Ctrl + F
全屏模式
F11
切换主题
Ctrl + Shift + D
显示快捷键
?
增大字号
Ctrl + =
减小字号
Ctrl + -