1 package fr.ove.openmath.mathematica;
2
3 import javax.swing.*;
4 import javax.swing.event.*;
5 import java.awt.*;
6 import java.awt.event.*;
7 import fr.ove.openmath.mathematica.*;
8 import fr.ove.openmath.mathematica.events.*;
9
10 public class BracketBullet extends JPanel {
11 /***
12 * The PanelJomes the instance will contain.
13 */
14 private PanelJomes panelJomes;
15
16 /***
17 * The width of the bracket line displayed.
18 */
19 private static final int width = 8;
20
21 /***
22 * The minimal of the instance.
23 */
24 int minHeight = 15;
25
26 /***
27 * Chesks if the instance is selected or not. <CODE>true</CODE> by default.
28 */
29 boolean isSelected = true;
30
31 /***
32 * The Constructor.
33 * @panel pj the PanelJomes contained by the instance.
34 */
35 public BracketBullet(PanelJomes pj) {
36 panelJomes = pj;
37
38 Font font = pj.getJomeRequest().getFont();
39 FontMetrics fm = getFontMetrics(font);
40 minHeight = fm.getHeight() + 4;
41
42 addMouseListener(
43 new MouseAdapter() {
44 public void mousePressed(MouseEvent event) {
45 PanelJomesEvent panelJomesEvent = new PanelJomesEvent(panelJomes);
46 panelJomesEvent.setAction(PanelJomesEvent.UPDATE, null);
47 panelJomes.firePanelJomesEvent(panelJomesEvent);
48
49 panelJomesEvent.setAction(PanelJomesEvent.UPDATE_SELECTION, null);
50 panelJomes.firePanelJomesEvent(panelJomesEvent);
51 }
52 }
53 );
54 }
55
56 /***
57 * Returns the preferred size of the instance.
58 */
59 public Dimension getPreferredSize() {
60 return new Dimension(width, (int) Math.max(minHeight, (panelJomes.getSize()).height));
61 }
62
63 /***
64 * Checks if the instance is selected.
65 * @param <CODE>true</CODE> if the instance is selected. <CODE>false</CODE> otherwise.
66 */
67 public boolean isSelected() {
68 return isSelected;
69 }
70
71 /***
72 * Sets the instance as selected or not.
73 * @param isSelected the selection sate.
74 */
75 public void setSelected(boolean isSelected) {
76 this.isSelected = isSelected;
77 repaint();
78 }
79
80 /***
81 * Paints the instance.
82 * @param g where to paint.
83 */
84 public void paint(Graphics g) {
85 Dimension size = getPreferredSize();
86 if (isSelected)
87 g.setColor(Color.red);
88 else
89 g.setColor(Color.black);
90
91 g.fillRect(4, 2, 2, size.height - 4);
92 g.fillRect(4, 2, width, 2);
93 g.fillRect(4, size.height - 4, width, 2);
94 }
95 }