equal
deleted
inserted
replaced
|
1 /*************************************************************************** |
|
2 Title: GraphBrowser/DefaultFontMetrics.java |
|
3 ID: $Id$ |
|
4 Author: Stefan Berghofer, TU Muenchen |
|
5 License: GPL (GNU GENERAL PUBLIC LICENSE) |
|
6 |
|
7 Default font metrics which is used when no graphics context |
|
8 is available. |
|
9 ***************************************************************************/ |
|
10 |
|
11 package GraphBrowser; |
|
12 |
|
13 import java.awt.*; |
|
14 |
|
15 public class DefaultFontMetrics extends FontMetrics |
|
16 { |
|
17 public DefaultFontMetrics(Font f) |
|
18 { super(f); } |
|
19 |
|
20 // note : values are rather inaccurate ! |
|
21 |
|
22 public int getLeading() |
|
23 { return 1; } |
|
24 |
|
25 public int getAscent() |
|
26 { return (int)(Math.round(font.getSize()*5.0/6.0)); } |
|
27 |
|
28 public int getDescent() |
|
29 { return (int)(Math.round(font.getSize()/6.0)); } |
|
30 |
|
31 public int stringWidth(String s) |
|
32 { return (int)(Math.round(s.length()*font.getSize()/2.0)); } |
|
33 } |