1 package fr.ove.openmath.jome.ctrlview.bidim;
2
3 import java.awt.*;
4 import fr.ove.openmath.jome.ctrlview.bidim.*;
5 import fr.ove.openmath.jome.ctrlview.bidim.selection.events.SelectionEvent;
6 import fr.ove.openmath.jome.model.*;
7
8 /***
9 * Layout manager that lays the display of an operator whose symbol is located between its 2 operands.<BR>
10 * Rendering is done vertically, the first operand on top, the symbol in the middle and the second operand
11 * under the 2 previous.
12 *
13 * @author © 1999 DIRAT Laurent
14 * @version 2.0 15/12/1999
15 */
16 public abstract class BetweenOperatorLayout extends VerticalCenteredLayout implements OperatorDisplayCreator {
17 /***
18 * According to the operator, the layout manager has to add some components (e.g. brackets, ...)
19 * or has to perform some "re-oganisation" before rendering.<BR>
20 * As soon as the layout manager is set to the display, this mehtod MUST be called with the display laid out
21 * as parameter. This method serves as well as a registering method. So all sub-classes of the instance MUST
22 * call super.initDisplay(displayToLay).
23 * @param displayToLay the display laid by the instance
24 */
25 public void initDisplay(Display displayToLay) {
26 super.initDisplay(displayToLay);
27 Display operatorDisplay = createOperatorDisplay();
28
29
30
31
32
33
34
35
36
37 operatorDisplay.addControlListener((FormulaTreeStructure) displayToLay.getListener());
38 this.displayToLay.add(operatorDisplay);
39 }
40
41 /***
42 * Checks the validity of the selection.
43 */
44 public void validateSelection() {
45 SelectionEvent selEvt = new SelectionEvent(displayToLay);
46
47
48
49
50 Display operatorDisplay = (Display) displayToLay.getComponent(0);
51 Display operand1 = (Display) displayToLay.getComponent(1);
52 Display operand2 = (Display) displayToLay.getComponent(2);
53 if ((operand1.gotSelectedElements() && operand2.gotSelectedElements()) ||
54 (operatorDisplay.isSelected())) {
55
56 displayToLay.select();
57
58 selEvt.setAction(SelectionEvent.PURGE, null);
59 displayToLay.fireSelectionEvent(selEvt);
60
61 selEvt.setAction(SelectionEvent.ADD, displayToLay);
62 displayToLay.fireSelectionEvent(selEvt);
63 }
64
65
66
67 Display display = displayToLay;
68 if (display.getParent() instanceof Display) {
69 display = (Display) display.getParent();
70 FormulaTreeStructure fts = (FormulaTreeStructure) display.getListener();
71 if (fts.getFather() != null)
72 ((DisplayLayout) display.getLayout()).validateSelection();
73 }
74
75
76 display.repaint();
77 }
78
79 /***
80 * Checks the validity of the deselection.
81 * @param display the display to deselect.
82 */
83 public void validateDeselection(Display display) {
84 Display father = displayToLay;
85 SelectionEvent selEvt = new SelectionEvent(father);
86
87
88 if (father.isSelected()) {
89 father.setNotSelected();
90
91 selEvt.setAction(SelectionEvent.REMOVE, father);
92 father.fireSelectionEvent(selEvt);
93
94 Display operatorDisplay = (Display) father.getComponent(0);
95 Display operand1 = (Display) father.getComponent(1);
96 Display operand2 = (Display) father.getComponent(2);
97
98 if (display == operand1) {
99 operatorDisplay.setNotSelected();
100 selEvt.setAction(SelectionEvent.ADD, operand2);
101 father.fireSelectionEvent(selEvt);
102 }
103 else if (display == operand2) {
104 operatorDisplay.setNotSelected();
105 selEvt.setAction(SelectionEvent.ADD, operand1);
106 father.fireSelectionEvent(selEvt);
107 }
108 else {
109 operand1.deselect();
110 operatorDisplay.setNotSelected();
111 operand2.deselect();
112 }
113
114
115 if (father.getParent() instanceof Display) {
116 father = (Display) father.getParent();
117 FormulaTreeStructure fts = (FormulaTreeStructure) father.getListener();
118 if (fts.getFather() != null)
119 ((DisplayLayout) father.getLayout()).validateDeselection(displayToLay);
120 }
121
122
123
124
125 validateSelection();
126
127
128 father.repaint();
129 }
130 }
131
132 /***
133 * Computes the size of the display according to its children size (if any),
134 * and its different attributes.
135 * @return the size of the display.
136 */
137 public Dimension computeAttributes() {
138 Display displayOperator = (Display) displayToLay.getComponent(0);
139 Display topOperand = (Display) displayToLay.getComponent(1);
140 Display bottomOperand = (Display) displayToLay.getComponent(2);
141
142 displayOperator.setShiftY(0);
143 topOperand.setShiftY(0);
144 bottomOperand.setShiftY(0);
145
146
147
148
149 Dimension dim = super.computeAttributes();
150
151
152
153 displayOperator.setShiftY(topOperand.getHeight());
154
155 topOperand.setShiftY(-displayOperator.getShiftY() - displayOperator.getHeight());
156 bottomOperand.setShiftY(displayOperator.getHeight());
157
158
159
160 int ascent = displayToLay.getFontMetrics(displayToLay.getFont()).getAscent();
161 ascent = (int) Math.round(((float) ascent)*0.388f);
162
163 ascent += topOperand.getShiftY() + topOperand.getHeight() +
164 displayOperator.getShiftY() + displayOperator.getAscent();
165
166 displayToLay.setAscent(ascent);
167 displayToLay.setDescent(dim.height - ascent);
168
169 displayToLay.setComputeAttributes(false);
170
171 return dim;
172 }
173
174 /***
175 * The display needs to be rebuilt. We do this.
176 */
177 public void rebuildDisplay() {
178 Display tmp;
179 Display listDisplay[] = new Display[2];
180
181 for (int i = 1; i <= 2; i++) {
182 tmp = (Display) displayToLay.getComponent(i);
183 tmp.setLocation(0,0);
184 listDisplay[((FormulaTreeStructure) tmp.getListener()).getRank()] = tmp;
185 }
186
187
188 tmp = (Display) displayToLay.getComponent(0);
189
190
191
192 tmp.setIsSymbolOperatorDisplay(false);
193
194
195
196 displayToLay.removeAllDisplays();
197
198
199 tmp.setIsSymbolOperatorDisplay(true);
200
201 displayToLay.add(tmp);
202
203 for (int i = 0; i < 2; i++)
204 displayToLay.add(listDisplay[i]);
205
206
207
208 displayToLay.computeAncestorsAttributes();
209 }
210 }