From 6ab8366d05c5e884329e746b5df1fa169661ec4b Mon Sep 17 00:00:00 2001 From: amwaterhouse Date: Wed, 9 Mar 2005 18:37:09 +0000 Subject: [PATCH 1/1] font chooser added --- src/jalview/gui/FontChooser.java | 59 ++++++++++++++++++ src/jalview/jbgui/GAlignFrame.java | 73 +++++------------------ src/jalview/jbgui/GFontChooser.java | 112 +++++++++++++++++++++++++++++++++++ 3 files changed, 186 insertions(+), 58 deletions(-) create mode 100755 src/jalview/gui/FontChooser.java create mode 100755 src/jalview/jbgui/GFontChooser.java diff --git a/src/jalview/gui/FontChooser.java b/src/jalview/gui/FontChooser.java new file mode 100755 index 0000000..782d2d6 --- /dev/null +++ b/src/jalview/gui/FontChooser.java @@ -0,0 +1,59 @@ +package jalview.gui; + +import jalview.jbgui.GFontChooser; +import jalview.gui.*; +import java.awt.*; +import java.awt.event.*; +import javax.swing.*; +import javax.swing.event.*; + + +public class FontChooser extends GFontChooser +{ + AlignmentPanel ap; + Font oldFont; + + public FontChooser(AlignmentPanel ap) + { + this.ap = ap; + + String fonts[] = java.awt.GraphicsEnvironment.getLocalGraphicsEnvironment().getAvailableFontFamilyNames(); + for(int i=0; i