1 package fr.ove.openmath.jome.ctrlview.bidim;
2
3 import java.awt.*;
4 import fr.ove.openmath.jome.ctrlview.bidim.Display;
5 import fr.ove.openmath.jome.ctrlview.bidim.DisplayLayout;
6 import fr.ove.openmath.jome.ctrlview.bidim.HorizontalLayout;
7 import fr.ove.openmath.jome.ctrlview.bidim.selection.events.SelectionEvent;
8 import fr.ove.openmath.jome.model.*;
9
10 /***
11 * A layout manager that lays components to place them as the different elements like the operator
12 * sum does.<BR>
13 * The different elements are contained in the display in the following order :
14 * <UL>
15 * <LI>the symbol of the operator.</LI>
16 * <LI>the expression.</LI>
17 * <LI>the lower bound.</LI>
18 * <LI>the upper bound.</LI>
19 *</UL>
20 *
21 * Bounds are optional elements.
22 *
23 * @author © 1999 DIRAT Laurent
24 * @version 2.0 16/12/1999
25 */
26 public abstract class MapsToSigmaLayout extends HorizontalLayout implements OperatorDisplayCreator {
27 /***
28 * According to the operator, the layout manager has to add some components (e.g. brackets, ...)
29 * or has to perform some "re-oganisation" before rendering.<BR>
30 * As soon as the layout manager is set to the display, this mehtod MUST be called with the display laid out
31 * as parameter. This method serves as well as a registering method. So all sub-classes of the instance MUST
32 * call super.initDisplay(displayToLay).
33 * @param displayToLay the display laid by the instance
34 */
35 public void initDisplay(Display displayToLay) {
36 super.initDisplay(displayToLay);
37
38 Display sigma = createOperatorDisplay();
39 sigma.addControlListener(this.displayToLay.getListener());
40 this.displayToLay.add(sigma);
41 }
42
43 /***
44 * Updates the level of the display that is layed out.<BR>
45 * @param level the level put to the display
46 */
47 public void updateLevel(int level) {
48 Display tmp;
49
50 if (displayToLay.getUpdateLevel()) {
51 displayToLay.updateChildrenLevel();
52
53
54 displayToLay.setLevel(level);
55 displayToLay.setUpdateLevel(false);
56
57
58 tmp = (Display) displayToLay.getComponent(0);
59 ((DisplayLayout) tmp.getLayout()).updateLevel(level);
60 tmp.setUpdateLevel(false);
61
62
63 tmp = (Display) displayToLay.getComponent(1);
64 ((DisplayLayout) tmp.getLayout()).updateLevel(level);
65 tmp.setUpdateLevel(false);
66
67 int count = displayToLay.getComponentCount();
68
69 if (count > 2) {
70
71 tmp = (Display) displayToLay.getComponent(2);
72 ((DisplayLayout) tmp.getLayout()).updateLevel(level+1);
73 tmp.setUpdateLevel(false);
74
75 if (count > 3) {
76
77 tmp = (Display) displayToLay.getComponent(3);
78 ((DisplayLayout) tmp.getLayout()).updateLevel(level+1);
79 tmp.setUpdateLevel(false);
80 }
81 }
82 }
83 }
84
85 /***
86 * Checks the validity of the selection.
87 * @param display the display to select.
88 */
89 public void validateSelection() {
90 Display symbol = (Display) displayToLay.getComponent(0);
91 Display expression = (Display) displayToLay.getComponent(1);
92
93 int count = displayToLay.getComponentCount();
94
95
96 if (symbol.isSelected())
97 displayToLay.select();
98 else if (count > 2) {
99 Display lower = (Display) displayToLay.getComponent(2);
100 Display upper;
101
102 if (lower.gotSelectedElements()) {
103 if (expression.gotSelectedElements())
104 displayToLay.select();
105 else if (count > 3) {
106 upper = (Display) displayToLay.getComponent(3);
107 if (upper.gotSelectedElements())
108 displayToLay.select();
109 }
110 }
111 else if (count > 3) {
112 upper = (Display) displayToLay.getComponent(3);
113 if (upper.gotSelectedElements()) {
114 if (expression.gotSelectedElements())
115 displayToLay.select();
116 }
117 }
118 }
119
120
121
122 if (displayToLay.isSelected()) {
123 SelectionEvent selEvt = new SelectionEvent(displayToLay);
124
125 selEvt.setAction(SelectionEvent.PURGE, null);
126 displayToLay.fireSelectionEvent(selEvt);
127
128 selEvt.setAction(SelectionEvent.ADD, displayToLay);
129 displayToLay.fireSelectionEvent(selEvt);
130 }
131
132
133
134 Display display = displayToLay;
135 if (display.getParent() instanceof Display) {
136 display = (Display) display.getParent();
137
138 FormulaTreeStructure fts = (FormulaTreeStructure) display.getListener();
139 if (fts.getFather() != null)
140 ((DisplayLayout) display.getLayout()).validateSelection();
141 }
142
143
144 display.repaint();
145 }
146
147 /***
148 * Checks the validity of the deselection.
149 * @param display the display to deselect.
150 */
151 public void validateDeselection(Display display) {
152 Display father = displayToLay;
153 SelectionEvent selEvt = new SelectionEvent(father);
154
155 if (father.isSelected()) {
156 father.setNotSelected();
157
158 selEvt.setAction(SelectionEvent.REMOVE, father);
159 father.fireSelectionEvent(selEvt);
160
161 Display expression = (Display) father.getComponent(1);
162 int count = father.getComponentCount();
163 if (display != expression) {
164
165
166 selEvt.setAction(SelectionEvent.ADD, expression);
167 father.fireSelectionEvent(selEvt);
168 }
169
170 ((Display) father.getComponent(0)).setNotSelected();
171 if (count > 2) {
172 ((Display) father.getComponent(2)).deselect();
173 if (count > 3)
174 ((Display) father.getComponent(3)).deselect();
175 }
176
177
178 if (father.getParent() instanceof Display) {
179 father = (Display) father.getParent();
180 FormulaTreeStructure fts = (FormulaTreeStructure) father.getListener();
181 if (fts.getFather() != null)
182 ((DisplayLayout) father.getLayout()).validateDeselection(displayToLay);
183 }
184
185
186
187 validateSelection();
188
189
190 father.repaint();
191 }
192 }
193
194 /***
195 * Computes the size of the display according to its children size (if any),
196 * and its different attributes.
197 * @return the size of the display.
198 */
199 public Dimension computeAttributes() {
200 int ascent = 0;
201 int descent = 0;
202
203 updateLevel(displayToLay.getLevel());
204
205 int width = 0;
206 int height = 0;
207
208 Display symbol, lower, expression, upper;
209 int gap = 2;
210
211
212 symbol = (Display) displayToLay.getComponent(0);
213 symbol.setSize(symbol.getPreferredSize());
214
215
216 expression = (Display) displayToLay.getComponent(1);
217 expression.setSize(expression.getPreferredSize());
218
219 int width1 = symbol.getWidth();
220
221 int count = displayToLay.getComponentCount();
222 if (count > 2) {
223
224 lower = (Display) displayToLay.getComponent(2);
225 lower.setSize(lower.getPreferredSize());
226 lower.setShiftY(symbol.getDescent() + lower.getAscent() + gap);
227
228 width1 = Math.max(lower.getWidth(), width1);
229
230 if (count > 3 ) {
231
232 upper = (Display) displayToLay.getComponent(3);
233 upper.setSize(upper.getPreferredSize());
234
235 width1 = Math.max(upper.getWidth(), width1);
236
237 upper.setShiftX(-(lower.getWidth() + upper.getWidth()) / 2);
238 upper.setShiftY(-(symbol.getAscent() + upper.getDescent() + gap));
239
240 ascent = symbol.getAscent() + upper.getHeight() + gap;
241 }
242 else {
243 ascent = symbol.getAscent();
244 }
245
246 symbol.setShiftX((width1 - symbol.getWidth()) / 2);
247 expression.setShiftX(gap + (width1 - symbol.getWidth())/2);
248
249 lower.setShiftX(-(symbol.getWidth() + lower.getWidth())/2 - (expression.getWidth() + expression.getShiftX()));
250
251 descent = symbol.getDescent() + lower.getHeight() + gap;
252 }
253 else {
254 ascent = symbol.getAscent();
255 descent = symbol.getDescent();
256 }
257
258 displayToLay.setAscent(ascent);
259 displayToLay.setDescent(descent);
260
261 width += width1 + expression.getWidth() + 4*gap;
262
263 height += ascent + descent;
264 displayToLay.setSize(width , height);
265
266 displayToLay.setComputeAttributes(false);
267 return new Dimension(width, height);
268 }
269
270 /***
271 * The display needs to be rebuilt. We do this.
272 */
273 public void rebuildDisplay() {
274
275
276
277
278
279 displayToLay.computeAncestorsAttributes();
280 }
281
282 }