View Javadoc

1   package fr.ove.openmath.jome.ctrlview.bidim;
2   
3   import java.awt.*;
4   import fr.ove.openmath.jome.ctrlview.bidim.DisplayLayout;
5   import fr.ove.openmath.jome.ctrlview.bidim.Display;
6   import fr.ove.openmath.jome.ctrlview.bidim.Bar;
7   import fr.ove.openmath.jome.ctrlview.bidim.selection.events.SelectionEvent;
8   import fr.ove.openmath.jome.model.*;
9   import fr.ove.utils.FontInfo;
10  
11  /***
12  * Layout manager that lays the display of the conjugate operator
13  *
14  * @author © 1999 DIRAT Laurent
15  * @version 2.0 15/12/1999
16  */
17  public class ConjugateLayout extends OverOperatorLayout {
18      /***
19      * Computes the size of the display according to its children size (if any),
20      * and its different attributes.
21      * @return the size of the display.
22      */
23      public Dimension computeAttributes() {
24          SymbolDisplay displayBar = null;
25          Bar bar = null;
26          
27          updateLevel(displayToLay.getLevel());
28              
29          // On est dans le cas particulier d'un symbol qui ne connais pas sa taille ? l'avance.
30          // Pour que cela puisse fonctionner correctement avec les autres displays, il faut qu'on
31          // lui precise sa preferred size.
32          // On met sa longueur ? 0 pour Èviter les Èlargissements infinis lors des diffÈrents retaillages
33          // dus aux dÈsiconifications.
34          displayBar = (SymbolDisplay) displayToLay.getComponent(0);
35          bar = (Bar) displayBar.getSymbol();
36          bar.setWidth(0);
37          bar.setHeight(FontInfo.getLineThickness(displayToLay, displayToLay.getFont())); // la hauteur fixe aussi ascent et descent        
38          
39          displayBar.setComputeAttributes(true);
40          displayBar.setShiftY(2);
41      
42          // On calcule les attributs des display enfants comme si 
43          // on avait affaire ? un VerticalCenteredLayout
44          Dimension dim = super.computeAttributes(); 
45          
46          // La diffÈrence rÈside en le calcul supplÈmentaire de la taille de la 
47          // barre que l'on ne peut fixer aprËs avoir calculÈ la largeur de l'argument
48          bar.setWidth(dim.width + 2);
49          displayBar.setSize(bar.getSize());
50                                                  
51          displayToLay.setAscent(((Display) displayToLay.getComponent(0)).getShiftY() +
52                    ((Display) displayToLay.getComponent(0)).getHeight() + 
53                    ((Display) displayToLay.getComponent(1)).getShiftY() +
54                    ((Display) displayToLay.getComponent(1)).getAscent());
55                    
56          displayToLay.setDescent(displayToLay.getHeight() - displayToLay.getAscent());
57          
58          displayToLay.setSize(dim);
59  
60          displayToLay.setComputeAttributes(false);
61          
62          return dim;
63      }
64      
65      /***
66      * Returns the display of the operator
67      */
68      public Display createOperatorDisplay() {
69          SymbolDisplay bar = new SymbolDisplay(displayToLay.getGraphicContext(), new Bar());
70          // Le display de la barre est le display d'un opÈrateur (on peut le considÈrer comme tel)
71          bar.setIsSymbolOperatorDisplay(true);
72          
73          return bar;
74      }
75  }