/* File: DefaultFont.java
 * Contains: Default Fonts
 * Author: Austin Tate <a.tate@ed.ac.uk>
 * Created: Thu Jan 15 16:39:25 1998
 * Updated: Mon Aug 24 16:52:54 1998 by Jeff Dalton
 * Copyright: (c) 1998, AIAI, University of Edinburgh
 */

package ix.util;

import java.awt.*;

public class DefaultFont {

    public static Font normal;
    public static Font bold;
    public static Font normalSuperscript;

    private static final int DEFAULT_SIZE=16; // was 12

    static {
	defaultFont();
    }

    public static void defaultFont () {
        setDefaultFontSize(DEFAULT_SIZE);
    }

    public static void setDefaultFontSize(int size) {
         int ssSize = (int) (size/3)*2;

	 normalSuperscript = new Font("SansSerif", Font.PLAIN, ssSize);
         normal = new Font("SansSerif", Font.PLAIN, size);
         bold = new Font("SansSerif", Font.BOLD, size);
    }

}