View Javadoc

1   package fr.ove.openmath.jome.ctrlview.bidim;
2   
3   import java.awt.*;
4   
5   /***
6   * The graphic context of each part of the formula to display.
7   *
8   * @author © 1998 DIRAT Laurent
9   * @version 1.0  22/06/98
10  */
11  public class GraphicContext implements java.io.Serializable {
12      /***
13      * The font used.
14      */
15      private Font font;
16      
17      /***
18      * The size of the font used.
19      */
20      private int sizeRef; // Serves as the reference font size for font scales.
21      
22      /***
23      * The color used to display the part of the formula.
24      */
25      private Color foregroundColor;
26      
27      /***
28      * The color used to display the background of the formula.
29      */
30      private Color backgroundColor;
31      
32      /***
33      * The color used to hilight the selected part.
34      */
35      private static Color selectionColor;
36      
37      /***
38      * How many times the scale factor is apply to reduce the font size.
39      */
40      private int nbTime = 0;
41      
42      /***
43      * The default constructor.<BR>
44      * The default is :
45      * <UL>
46      * <LI> a Times New Roman font, regular, with a size of 14 </LI>
47      * <LI> the foreground color set to black </LI>
48      * <LI> the background color set to white </LI>
49      * <LI> the selection color set to yellow </LI>
50      * </UL>
51      */
52      public GraphicContext() {
53          this(new Font("Times New Roman", Font.PLAIN, 14), Color.black, Color.white, Color.yellow);
54      }
55      
56      /***
57      * The Constructor.
58      *
59      * @param font the font used to display all the text elements.
60      * @param color the color used to display all the text elements.
61      * @param background the color used as background for the display.
62      * @param selectionColor the color of all the selected elements.
63      */
64      public GraphicContext(Font font, Color foregroundColor, Color backgroundColor, Color selectionColor) {
65          this.font = font;
66          sizeRef = font.getSize();
67          this.foregroundColor = foregroundColor;
68          this.backgroundColor = backgroundColor;
69          this.selectionColor = selectionColor;
70      }
71      
72      /***
73      * The constructor by copy.
74      * @param gc the graphic context to copy.
75      */
76      public GraphicContext(GraphicContext gc) {
77          font = gc.getFont();
78          sizeRef = gc.getSizeRef();
79          foregroundColor = gc.getForegroundColor();
80          backgroundColor = gc.getBackgroundColor();
81          selectionColor = gc.getSelectionColor();
82      }
83      
84      // ### The getters ###
85      
86      /***
87      * Returns the font used in the graphic context.
88      */
89      public Font getFont() {
90          return font;
91      }
92      
93      /***
94      * Returns the reference size of the font.
95      */
96      public int getSizeRef() {
97          return sizeRef;
98      }
99      
100     /***
101     * Returns the color used by the graphic context.
102     */
103     public Color getForegroundColor() {
104         return foregroundColor;
105     }
106     
107     /***
108     * Returns the background for the display.
109     */
110     public Color getBackgroundColor() {
111         return backgroundColor;
112     }
113     
114     /***
115     * Returns the color used in the graphic context to hilight the selection.
116     * @return the color.
117     */
118     public Color getSelectionColor() {
119         return selectionColor;
120     }
121     
122     // ### The setters ###
123     
124     /***
125     * Sets a new font to the context.
126     * @param font the new font.
127     */
128     public void setFont(Font font) {
129         this.font = font;
130         sizeRef = font.getSize();
131     }
132     
133     /***
134     * Sets a new color to the context.
135     * @param color the new color.
136     */
137     public void setForegroundColor(Color foregroundColor) {
138         this.foregroundColor = foregroundColor;
139     }
140     
141     /***
142     * Sets a new background color for the display.
143     * @param background the color used as background for the display.
144     */
145     public void setBackgroundColor(Color backgroundColor) {
146         this.backgroundColor = backgroundColor;
147     }
148     
149     /***
150     * Sets a new selection color to the context.
151     * @param selectionColor the new color.
152     */
153     public void setSelectionColor(Color selectionColor) {
154         this.selectionColor = selectionColor;
155     }
156     
157     /***
158     * Scales the current font.
159     * @param nbTime how many the scale factor is applied.
160     * @return the font scaled.
161     */
162     public Font scaleFont(int nbTime) {
163         if (this.nbTime != nbTime) {
164             String name = font.getName();
165             int style = font.getStyle();
166             int size = sizeRef;
167             
168             this.nbTime = nbTime;
169             
170             for (int i = 0; i < nbTime; i++) {
171                 size = (int) Math.round( ((float) size) * 0.7f );
172                 if (size < 10)
173                     break;
174             }
175             
176             size = (size < 10) ? 10 : size;
177             
178             font = new Font(name, style, size);
179         }
180         
181         return font;
182     }
183     
184 }