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  * A layout manager that lays components to be displayed as a fraction.
13  *
14  * @author © 1999 DIRAT Laurent
15  * @version 2.0 15/12/1999
16  */
17  public class FractionLayout extends BetweenOperatorLayout {
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 fractionBar = null;
26          
27          updateLevel(displayToLay.getLevel());
28          
29          // On est dans le cas particulier d'un symbol qui ne connait 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. (On rajoute 8 pixels ? sa largeur un peu plus bas)
34          displayBar = (SymbolDisplay) displayToLay.getComponent(0);
35          displayBar.setWidth(0);
36          fractionBar = (Bar) displayBar.getSymbol();
37          fractionBar.setWidth(0);
38          
39          fractionBar.setHeight(FontInfo.getLineThickness(displayToLay, displayToLay.getFont())); // la hauteur fixe aussi ascent et descent
40          
41          displayBar.setComputeAttributes(true);
42      
43          // On calcule les attributs des display enfants comme si 
44          // on avait affaire ? un VerticalCenteredLayout
45          Dimension dim = super.computeAttributes(); 
46          
47          // La diffÈrence rÈside en le calcul supplÈmentaire de la taille de la 
48          // de fraction que l'on ne peut fixer aprËs avoir calculÈ la largeur
49          // du numÈrateur et du dÈnominateur
50          fractionBar.setWidth(dim.width + 8);
51          displayBar.setSize(fractionBar.getSize());
52          
53          dim.width = displayBar.getWidth();
54          displayToLay.setSize(dim);
55          
56          return dim;
57      }
58      
59      /***
60      * Returns the display of the operator
61      */
62      public Display createOperatorDisplay() {
63          SymbolDisplay fractionBar = new SymbolDisplay(displayToLay.getGraphicContext(), new Bar());
64          // Le display de la barre de fraction est le display d'un opÈrateur (on peut le considÈrer comme tel)
65          fractionBar.setIsSymbolOperatorDisplay(true);
66          
67          return fractionBar;
68      }    
69  }