Source code: org/gjt/sp/jedit/gui/MarkersMenu.java
1 /*
2 * MarkersMenu.java - Markers menu
3 * :tabSize=8:indentSize=8:noTabs=false:
4 * :folding=explicit:collapseFolds=1:
5 *
6 * Copyright (C) 2001 Slava Pestov
7 *
8 * This program is free software; you can redistribute it and/or
9 * modify it under the terms of the GNU General Public License
10 * as published by the Free Software Foundation; either version 2
11 * of the License, or any later version.
12 *
13 * This program is distributed in the hope that it will be useful,
14 * but WITHOUT ANY WARRANTY; without even the implied warranty of
15 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
16 * GNU General Public License for more details.
17 *
18 * You should have received a copy of the GNU General Public License
19 * along with this program; if not, write to the Free Software
20 * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
21 */
22
23 package org.gjt.sp.jedit.gui;
24
25 //{{{ Imports
26 import javax.swing.event.*;
27 import javax.swing.*;
28 import java.awt.event.*;
29 import java.awt.*;
30 import java.util.*;
31 import org.gjt.sp.jedit.*;
32 //}}}
33
34 public class MarkersMenu extends EnhancedMenu
35 {
36 //{{{ MarkersMenu constructor
37 public MarkersMenu()
38 {
39 super("markers");
40 } //}}}
41
42 //{{{ menuSelected() method
43 public void menuSelected(MenuEvent evt)
44 {
45 super.menuSelected(evt);
46 final View view = GUIUtilities.getView(this);
47
48 if(getMenuComponentCount() != 0)
49 {
50 for(int i = getMenuComponentCount() - 1;
51 i >= 0;
52 i--)
53 {
54 Component comp = getMenuComponent(i);
55 if(comp instanceof JSeparator)
56 break;
57 else
58 remove(comp);
59 }
60 }
61
62 Buffer buffer = view.getBuffer();
63
64 Vector markers = buffer.getMarkers();
65
66 if(markers.size() == 0)
67 {
68 JMenuItem mi = new JMenuItem(jEdit.getProperty(
69 "no-markers.label"));
70 mi.setEnabled(false);
71 add(mi);
72 return;
73 }
74
75 int maxItems = jEdit.getIntegerProperty("menu.spillover",20);
76
77 JMenu current = this;
78
79 for(int i = 0; i < markers.size(); i++)
80 {
81 final Marker marker = (Marker)markers.elementAt(i);
82 int lineNo = buffer.getLineOfOffset(marker.getPosition());
83
84 if(current.getItemCount() >= maxItems && i != markers.size() - 1)
85 {
86 //current.addSeparator();
87 JMenu newCurrent = new JMenu(
88 jEdit.getProperty(
89 "common.more"));
90 current.add(newCurrent);
91 current = newCurrent;
92 }
93
94 JMenuItem mi = new MarkersMenuItem(buffer,
95 lineNo,marker.getShortcut());
96 mi.addActionListener(new ActionListener()
97 {
98 public void actionPerformed(ActionEvent evt)
99 {
100 view.getTextArea().setCaretPosition(
101 marker.getPosition());
102 }
103 });
104 current.add(mi);
105 }
106 } //}}}
107
108 public void menuDeselected(MenuEvent e) {}
109
110 public void menuCanceled(MenuEvent e) {}
111
112 //{{{ MarkersMenuItem class
113 static class MarkersMenuItem extends JMenuItem
114 {
115 //{{{ MarkersMenuItem constructor
116 MarkersMenuItem(Buffer buffer, int lineNo, char shortcut)
117 {
118 String text = buffer.getLineText(lineNo).trim();
119 if(text.length() == 0)
120 text = jEdit.getProperty("markers.blank-line");
121 setText((lineNo + 1) + ": " + text);
122
123 shortcutProp = "goto-marker.shortcut";
124 MarkersMenuItem.this.shortcut = shortcut;
125 } //}}}
126
127 //{{{ getPreferredSize() method
128 public Dimension getPreferredSize()
129 {
130 Dimension d = super.getPreferredSize();
131
132 String shortcut = getShortcut();
133
134 if(shortcut != null)
135 {
136 d.width += (getFontMetrics(acceleratorFont)
137 .stringWidth(shortcut) + 15);
138 }
139 return d;
140 } //}}}
141
142 //{{{ paint() method
143 public void paint(Graphics g)
144 {
145 super.paint(g);
146
147 String shortcut = getShortcut();
148
149 if(shortcut != null)
150 {
151 g.setFont(acceleratorFont);
152 g.setColor(getModel().isArmed() ?
153 acceleratorSelectionForeground :
154 acceleratorForeground);
155 FontMetrics fm = g.getFontMetrics();
156 Insets insets = getInsets();
157 g.drawString(shortcut,getWidth() - (fm.stringWidth(
158 shortcut) + insets.right + insets.left + 5),
159 getFont().getSize() + (insets.top - 1)
160 /* XXX magic number */);
161 }
162 } //}}}
163
164 //{{{ Private members
165 private String shortcutProp;
166 private char shortcut;
167 private static Font acceleratorFont;
168 private static Color acceleratorForeground;
169 private static Color acceleratorSelectionForeground;
170
171 //{{{ getShortcut() method
172 private String getShortcut()
173 {
174 if(shortcut == '\0')
175 return null;
176 else
177 {
178 String shortcutPrefix = jEdit.getProperty(shortcutProp);
179
180 if(shortcutPrefix == null)
181 return null;
182 else
183 {
184 return shortcutPrefix + " " + shortcut;
185 }
186 }
187 } //}}}
188
189 //{{{ Class initializer
190 static
191 {
192 acceleratorFont = UIManager.getFont("MenuItem.acceleratorFont");
193 acceleratorFont = new Font("Monospaced",
194 acceleratorFont.getStyle(),
195 acceleratorFont.getSize());
196 acceleratorForeground = UIManager
197 .getColor("MenuItem.acceleratorForeground");
198 acceleratorSelectionForeground = UIManager
199 .getColor("MenuItem.acceleratorSelectionForeground");
200 } //}}}
201
202 //}}}
203 } //}}}
204 }