View Javadoc

1   package fr.ove.openmath.jome.ctrlview.bidim;
2   
3   import java.awt.*;
4   import java.util.*;
5   import fr.ove.openmath.jome.ctrlview.bidim.Display;
6   import fr.ove.openmath.jome.ctrlview.bidim.DisplayLayout;
7   import fr.ove.openmath.jome.ctrlview.bidim.selection.events.SelectionEvent;
8   import fr.ove.openmath.jome.model.*;
9   
10  /***
11  *
12  * @author © 1999 DIRAT Laurent
13  * @version 2.0 17/12/1999
14  */
15  public class RequestLayout extends HorizontalLayout {
16      /***
17      * Do we need to insert separator display ?
18      */
19      private boolean insertSeparatorDisplay = true;
20      
21      /***
22      * The number of the components al ready present before an other insertion
23      * or removal. This is necessary to keep in mind this, in order to know if 
24      * we must parse the list of components to check if we have to insert symbol
25      * display or not.
26      */
27      private int prevNbComponent = 0;
28      
29      private String opeSymbol;
30      
31      private Display displaySlot = null;
32      
33      /***
34      * Inserts, if necessary, a display of the operator symbol that the display
35      * laid by the instance represents.
36      */
37      public void insertOperatorDisplay() {
38          Display current, next;
39          FormulaTreeStructure fatherFts = (FormulaTreeStructure) displayToLay.getListener();
40          FormulaTreeStructure fts;
41          StringDisplay stringDisplay;
42          int nbComponent = displayToLay.getComponentCount();
43          
44          if (nbComponent > 1) {
45              if (fatherFts.getResourceIdentifier().equals("request"))
46                  opeSymbol = new String("  with  ");
47              else
48                  opeSymbol = new String("  if  ");
49                  
50              stringDisplay = new StringDisplay(displayToLay.getGraphicContext(), opeSymbol, true);
51              stringDisplay.addControlListener(fatherFts);
52              displayToLay.add(stringDisplay, stringDisplay, 1);
53              nbComponent++;
54          } 
55          
56          // Mise ? jour du nombre de components prÈsents dans le display.
57          prevNbComponent = displayToLay.getComponentCount();
58          // On n'a plus besoin d'insÈrer des displays d'opÈrateur.
59          insertSeparatorDisplay = false;
60          // On a rajoutÈ un display, on demande le recalcul de tous les ancÍtres
61          // de l'instance.
62          displayToLay.computeAncestorsAttributes();
63      }
64      
65      /***
66      * Checks the validity of the selection.
67      */
68      public void validateSelection() {
69      }
70      
71      /***
72      * Checks the validity of the deselection.
73      * @param display the display to deselect.
74      */
75      public void validateDeselection(Display display) {
76      }
77      
78      /***
79      * Computes the size of the display according to its children size (if any),
80      * and its different attributes.
81      * @return the size of the display.
82      */
83      public Dimension computeAttributes() {
84          int ascent = 0;
85          int descent = 0;
86          
87          //Always add the container's insets!
88          Insets insets = displayToLay.getParent().insets();
89          int width = insets.left + insets.right;
90          int height = insets.top + insets.bottom;
91          
92          Display tmp;
93          
94          int count = displayToLay.getComponentCount();
95          Slot slot;
96          Constant cte;
97          int stop = 2;
98          
99          if (count == 1) {
100             if (displaySlot != null) {
101                 slot = (Slot) displaySlot.getListener();
102                 if (slot.getChild(0) instanceof Constant) {
103                     cte = (Constant) slot.getChild(0);
104                     if (!cte.isTemplate()) {
105                         displayToLay.add(displaySlot);
106                         stop = 2;
107                     }
108                 }
109                 else
110                     stop = 1;
111             }
112         }
113         else if (count == 2) {
114             displaySlot = (Display) displayToLay.getComponent(1);
115             slot = (Slot) displaySlot.getListener();
116             if (slot.getChild(0) instanceof Constant) {
117                 cte = (Constant) slot.getChild(0);
118                 if (cte.isTemplate()) {
119                     displayToLay.remove(displaySlot);
120                     stop = 1;
121                 }
122             }
123             else 
124                 stop = 2;
125         }
126         
127         
128         // On regarde si le nombre de component dans le display a chnagÈ depuis
129         // la derniËre fois. Si oui, il faut contrÙler s'il ne faut pas ajouter
130         // des display d'opÈrateur.
131         if (insertSeparatorDisplay || (prevNbComponent != ((Display) displayToLay).getComponentCount()))
132             insertOperatorDisplay();
133         
134         updateLevel(displayToLay.getLevel());
135         
136         count = displayToLay.getComponentCount();
137         stop = (count > 1) ? 2 : 1;
138         
139         // Ca va de la condition au with ou if selon le type
140         for (int i = 0; i < stop; i++) {
141             tmp = (Display) displayToLay.getComponent(i);
142             tmp.setSize(tmp.getPreferredSize());
143                     
144             width += tmp.getWidth() + tmp.getShiftX();
145                     
146             ascent = Math.max(tmp.getAscent() - tmp.getShiftY(),
147                               ascent);
148                       
149             descent = Math.max(tmp.getDescent() + tmp.getShiftY(),
150                                descent);
151                                 
152         }
153         
154         
155         if (count == 3) {
156             tmp = (Display) displayToLay.getComponent(2);
157             tmp.setSize(tmp.getPreferredSize());
158             height = (int) Math.max(((Display) displayToLay.getComponent(0)).getHeight(), 
159                                     ((Display) displayToLay.getComponent(2)).getHeight());
160             width += tmp.getWidth() + tmp.getShiftX();
161             displayToLay.setAscent(Math.max( ((Display) displayToLay.getComponent(0)).getAscent(), 
162                                              ((Display) displayToLay.getComponent(2)).getAscent() ));
163         }
164         else {
165             height = ((Display) displayToLay.getComponent(0)).getHeight();
166             int shiftY = ((Display) displayToLay.getComponent(0)).getDescent();
167             //count = displayToLay.getComponentCount();
168             for (int i = 2; i < count; i++) {
169                 tmp = (Display) displayToLay.getComponent(i);
170                 tmp.setSize(tmp.getPreferredSize());
171                 
172                 if (i == 2) {
173                     if (count > 3) {
174                         // On fait en sorte que cet ÈlÈment commence ? 20 pixels du bord gauche du display le contenant
175                         tmp.setShiftX(-width + 20 );
176                         shiftY += tmp.getAscent()+ 10;
177                         tmp.setShiftY(shiftY);
178                     }
179                     else
180                         width += tmp.getWidth();
181                 }
182                 else {
183                     tmp.setShiftX(-((Display) displayToLay.getComponent(i-1)).getWidth());
184                     shiftY += ((Display) displayToLay.getComponent(i-1)).getDescent() + tmp.getAscent()+ 5;
185                     tmp.setShiftY(shiftY);
186                 }
187                 
188                 width = Math.max(width, 20 + tmp.getWidth());
189                 
190                 if (i == (count - 1))
191                     height = shiftY + tmp.getHeight();
192             }
193             
194             displayToLay.setAscent(Math.max( 0, ((Display) displayToLay.getComponent(0)).getAscent() ));
195         }
196         
197         displayToLay.setSize(width , height);
198         displayToLay.setDescent(height - displayToLay.getAscent());
199         
200         displayToLay.setComputeAttributes(false);
201         
202         return new Dimension(width, height);
203     }
204 
205     /*
206      * Lays out the container in the specified panel.
207      * @param parent the component which needs to be laid out 
208      */
209      public void layoutContainer(Container parent) {
210         // On regarde si le nombre de component dans le display a chnagÈ depuis
211         // la derniËre fois. Si oui, il faut contrÙler s'il ne faut pas ajouter
212         // des display d'opÈrateur.
213         if (insertSeparatorDisplay || (prevNbComponent != ((Display) parent).getComponentCount()))
214             insertOperatorDisplay();
215         
216         super.layoutContainer(parent);
217     }
218     
219 
220     /***
221     * The display needs to be rebuilt. We do this.
222     */
223     public void rebuildDisplay() {
224         Display tmp;
225         int nbDisplay = ((FormulaTreeStructure) displayToLay.getListener()).getNbChildren();
226         Display listDisplay[] = new Display[nbDisplay];
227         
228         for (int i = 0; i < displayToLay.getComponentCount(); i++) {
229             tmp = (Display) displayToLay.getComponent(i);
230             if (!tmp.isSymbolOperatorDisplay()) {
231                 // A voir !!!!!
232                 // Mais il semblerai que bon, sinon ? la (re)construction du display il se base
233                 // sur des anciennes valeurs, et donc pas tarrible niveau affichage.
234                 tmp.setLocation(0, 0);
235                 listDisplay[((FormulaTreeStructure) tmp.getListener()).getRank()] = tmp;
236             }
237         }
238         
239         // ATTENTION : ici, on enlËve les displays fils de display, mais on ne les enlËve pas de la liste
240         // des listeners de la fts qu'il sont en train d'Ècouter. Exception faite pour les displays d'opÈrateur.
241         displayToLay.removeAllDisplays();
242         
243         for (int i = 0; i < nbDisplay; i++)
244             displayToLay.add(listDisplay[i]);
245             
246         // On a reconstruit le display, il faut maintenant insÈrer les displays d'opÈrateur.
247         insertSeparatorDisplay = true;
248     }
249    
250 }