Font metrics used for batch mode layout (without X11 connection).
authorberghofe
Tue Oct 16 16:48:30 2001 +0200 (2001-10-16)
changeset 11799533a95523f61
parent 11798 fbab70de9b0d
child 11800 5f84c687ba06
Font metrics used for batch mode layout (without X11 connection).
lib/browser/GraphBrowser/DefaultFontMetrics.java
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/lib/browser/GraphBrowser/DefaultFontMetrics.java	Tue Oct 16 16:48:30 2001 +0200
     1.3 @@ -0,0 +1,33 @@
     1.4 +/***************************************************************************
     1.5 +  Title:      GraphBrowser/DefaultFontMetrics.java
     1.6 +  ID:         $Id$
     1.7 +  Author:     Stefan Berghofer, TU Muenchen
     1.8 +  License:    GPL (GNU GENERAL PUBLIC LICENSE)
     1.9 +
    1.10 +  Default font metrics which is used when no graphics context
    1.11 +  is available.
    1.12 +***************************************************************************/
    1.13 +
    1.14 +package GraphBrowser;
    1.15 +
    1.16 +import java.awt.*;
    1.17 +
    1.18 +public class DefaultFontMetrics extends FontMetrics
    1.19 +{
    1.20 +	public DefaultFontMetrics(Font f)
    1.21 +	{ super(f); }
    1.22 +
    1.23 +	// note : values are rather inaccurate !
    1.24 +
    1.25 +	public int getLeading()
    1.26 +	{ return 1; }
    1.27 +
    1.28 +	public int getAscent()
    1.29 +	{ return (int)(Math.round(font.getSize()*5.0/6.0)); }
    1.30 +
    1.31 +	public int getDescent()
    1.32 +	{ return (int)(Math.round(font.getSize()/6.0)); }
    1.33 +
    1.34 +	public int stringWidth(String s)
    1.35 +	{ return (int)(Math.round(s.length()*font.getSize()/2.0)); }
    1.36 +}