1 package fr.ove.openmath.mfd2;
2
3 import java.awt.*;
4 import java.awt.event.*;
5 import java.io.*;
6 import java.util.Vector;
7 import fr.ove.openmath.jome.Jome;
8 import fr.ove.openmath.exceptions.*;
9 import fr.ove.openmath.mfd2.events.*;
10
11 public class PanelJomes extends Panel implements OpenMathResultSetable {
12 private Bullet bullet;
13
14
15 private Panel panelRequest;
16 private Jome jomeRequest;
17
18
19 private Panel panelResult;
20 private Jome jomeResult;
21
22
23 private Vector listeners = new Vector();
24
25 /***
26 * The constructor.
27 */
28 public PanelJomes() {
29 super();
30
31
32
33
34 setLayout(new BorderLayout(0, 0));
35
36 Panel mainPanel = new Panel();
37 mainPanel.setLayout(new BorderLayout(0, 0));
38 add("Center", mainPanel);
39
40
41 panelRequest = new Panel(new FlowLayout(FlowLayout.LEFT, 5, 4));
42
43 jomeRequest = new Jome();
44 jomeRequest.setDrawBounds(false);
45 jomeRequest.setFont(new java.awt.Font("Times New Roman", java.awt.Font.PLAIN, 18));
46 jomeRequest.setShiftX(0);
47 jomeRequest.setShiftY(0);
48 panelRequest.add(jomeRequest);
49
50
51 panelResult = new Panel(new FlowLayout(FlowLayout.CENTER, 0, 0));
52
53 jomeResult = new Jome();
54 jomeResult.setDrawBounds(false);
55 jomeResult.setShiftX(0);
56 jomeResult.setShiftY(0);
57 jomeResult.setFont(new java.awt.Font("Times New Roman",java.awt.Font.PLAIN,12));
58 panelResult.add(jomeResult);
59
60 mainPanel.add("North", panelRequest);
61 mainPanel.add("Center", panelResult);
62
63 try {
64 bullet = new Bullet(this);
65 add("West", bullet);
66 }
67 catch (Exception e) {
68 e.printStackTrace();
69 }
70 }
71
72 public boolean isSelected() {
73 return bullet.isSelected();
74 }
75
76 public void setSelected(boolean isSelected) {
77 bullet.setSelected(isSelected);
78 }
79
80
81
82 /***
83 * Sets the request. (under its linear form)
84 * @param request the request.
85 */
86 public void setLinearRequest(String request) {
87 if (!request.equals(jomeRequest.getLinear())) {
88 jomeRequest.setLinear(request);
89
90 PanelJomesEvent event = new PanelJomesEvent(this);
91 event.setAction(PanelJomesEvent.UPDATE_REQUEST, null);
92 firePanelJomesEvent(event);
93 }
94 }
95
96 /***
97 * Returns the request. (under its linear form)
98 */
99 public String getLinearRequest() {
100 return jomeRequest.getLinear();
101 }
102
103 /***
104 * Sets the request. (under its OpenMath form)
105 * @param request the request.
106 */
107 public void setOpenMathRequest(String request) throws ErrorMessageException {
108 try {
109 jomeRequest.setOpenMath(request);
110
111 PanelJomesEvent event = new PanelJomesEvent(this);
112 event.setAction(PanelJomesEvent.UPDATE_REQUEST, null);
113 firePanelJomesEvent(event);
114 }
115 catch(Exception e) {
116 throw((ErrorMessageException) e);
117 }
118 }
119
120 /***
121 * Returns the request. (under its OpenMath form)
122 */
123 public String getOpenMathRequest() {
124 return jomeRequest.getOpenMath();
125 }
126
127
128
129 /***
130 * Sets the result. (under its linear form)
131 * @param result the result.
132 */
133 public void setLinearResult(String result) {
134 jomeResult.setLinear(result);
135
136 PanelJomesEvent event = new PanelJomesEvent(this);
137 event.setAction(PanelJomesEvent.UPDATE_RESULT, null);
138 firePanelJomesEvent(event);
139 }
140
141 /***
142 * Returns the result. (under its linear form)
143 */
144 public String getLinearResult() {
145 return jomeResult.getLinear();
146 }
147
148 public Jome getJomeResult() {
149 return jomeResult;
150 }
151
152 public Jome getJomeRequest() {
153 return jomeRequest;
154 }
155
156 /***
157 * Sets the result. (under its OpenMath form)
158 * @param result the result.
159 */
160 public void setOpenMathResult(String result) throws ErrorMessageException {
161 try {
162 jomeResult.setOpenMath(result);
163
164 PanelJomesEvent event = new PanelJomesEvent(this);
165 event.setAction(PanelJomesEvent.UPDATE_RESULT, null);
166 firePanelJomesEvent(event);
167 }
168 catch (Exception e) {
169 throw((ErrorMessageException) e);
170 }
171 }
172
173 /***
174 * Returns the result. (under its OpenMath form)
175 */
176 public String getOpenMathResult() {
177 return jomeResult.getOpenMath();
178 }
179
180 /***
181 */
182 public void addPanelJomesListener(PanelJomesListener panelJomesListener) {
183 listeners.addElement(panelJomesListener);
184 }
185
186 /***
187 */
188 public void removePanelJomesListener(PanelJomesListener panelJomesListener) {
189 listeners.removeElement(panelJomesListener);
190 }
191
192 /***
193 */
194 public void removeAllPanelJomesListener() {
195 listeners.setSize(0);
196 }
197
198 /***
199 * Fires a PanelJomesEvent event to registered listeners.
200 * @param panelJomesEvent event encapsulating relevant information.
201 */
202 public void firePanelJomesEvent(PanelJomesEvent panelJomesEvent) {
203 for (int i = 0; i < listeners.size(); i++)
204 ((PanelJomesListener)listeners.elementAt(i)).consumePanelJomesEvent(panelJomesEvent);
205 }
206
207
208 private class Bullet extends Panel {
209 PanelJomes panelJomes;
210 int width = 8;
211 int minHeight = 15;
212 boolean isSelected = true;
213
214 public Bullet(PanelJomes pj) throws Exception {
215 panelJomes = pj;
216
217 Font font = pj.getJomeRequest().getFont();
218 FontMetrics fm = getFontMetrics(font);
219 minHeight = fm.getHeight() + 4;
220 addMouseListener(
221 new MouseAdapter() {
222 public void mousePressed(MouseEvent event) {
223 PanelJomesEvent panelJomesEvent = new PanelJomesEvent(panelJomes);
224 panelJomesEvent.setAction(PanelJomesEvent.UPDATE, null);
225 panelJomes.firePanelJomesEvent(panelJomesEvent);
226
227 panelJomesEvent.setAction(PanelJomesEvent.UPDATE_SELECTION, null);
228 panelJomes.firePanelJomesEvent(panelJomesEvent);
229 }
230 }
231 );
232 }
233
234 public Dimension getPreferredSize() {
235 return new Dimension(width, (int) Math.max(minHeight, (panelJomes.getSize()).height));
236 }
237
238 public boolean isSelected() {
239 return isSelected;
240 }
241
242 public void setSelected(boolean isSelected) {
243 this.isSelected = isSelected;
244 repaint();
245 }
246
247 public void paint(Graphics g) {
248 Dimension size = getPreferredSize();
249 if (isSelected)
250 g.setColor(Color.red);
251 else
252 g.setColor(Color.black);
253
254 g.fillRect(4, 2, 2, size.height - 4);
255 g.fillRect(4, 2, width, 2);
256 g.fillRect(4, size.height - 4, width, 2);
257 }
258 }
259
260
261 }