View Javadoc

1   package fr.ove.openmath.jome.ctrlview.bidim;
2   
3   import java.awt.*;
4   import fr.ove.openmath.jome.ctrlview.bidim.DisplayableImpl;
5   import fr.ove.utils.FontInfo;
6   
7   /***
8   * The bracket symbol for rendering interval. (i.e. symbol [ or ])
9   *
10  * @author © 1999 DIRAT Laurent
11  * @version 2.0 06/09/1999
12  */
13  public class SquaredBracketSymbol extends DisplayableImpl {
14      /***
15      * The character (i.e. '[' or ']') represented by the instance
16      * By default, the instance represents '['.
17      */
18      private char character;
19      
20      /***
21      * The thickness of the line to draw the symbol.
22      */
23      private int thickness;
24      
25      /***
26      *
27      */
28      private Component component;
29      
30      /***
31      * The constructor.
32      * @param character the associated character (i.e. '[' or ']') to the instance
33      **/
34      public SquaredBracketSymbol(char character, Component component) {
35          this.character = character;
36          this.component = component;
37      }
38      
39      /***
40      * The constructor.
41      * @param character the string representation of the associated character (i.e. '[' or ']') to the instance
42      **/
43      public SquaredBracketSymbol(String character, Component component) {
44          this.character = character.charAt(0);
45          this.component = component;
46      }
47      
48      /***
49      * Sets the thickness of the line to draw the symbol
50      * @param thickness the thickness to draw the symbol 
51      */
52      public void setThickness(int thickness) {
53          this.thickness = thickness;
54      }
55      
56      /***
57      * Returns the preferred size of the display.
58      */
59      public Dimension getPreferredSize() {
60          return new Dimension(FontInfo.getStringWidth(component, getGraphicContext().getFont(), "[") + 6, getHeight());
61      }
62      
63      public Dimension getSize() {
64          return getPreferredSize();
65      }
66      
67      
68      /***
69      * The paint method of the object to display.
70      * @param g the drawing area of the symbol.
71      */
72      public void paint(Graphics g) {
73          Dimension size = getSize();
74          // La barre horizontale du haut
75          g.fillRect(0+3, 0, size.width-6, thickness);
76          // La barre horizontale du bas
77          g.fillRect(0+3, size.height - thickness, size.width-6, thickness);
78          
79          // La barre verticale
80          if (character == '[')
81              g.fillRect(0+3, 0, thickness, size.height);
82          else
83              g.fillRect(size.width - thickness - 3, 0, thickness, size.height);
84      }
85  }