From: jprocter Date: Mon, 26 Apr 2010 10:00:53 +0000 (+0000) Subject: new applet parameters: heightScale and widthScale X-Git-Tag: Release_2_5~44 X-Git-Url: http://source.jalview.org/gitweb/?a=commitdiff_plain;h=742adcf2a22d9e7b8e8c9a6cf0dad5bab09e3b39;p=jalview.git new applet parameters: heightScale and widthScale --- diff --git a/src/jalview/appletgui/AlignViewport.java b/src/jalview/appletgui/AlignViewport.java index 684e005..8e80376 100755 --- a/src/jalview/appletgui/AlignViewport.java +++ b/src/jalview/appletgui/AlignViewport.java @@ -150,6 +150,46 @@ public class AlignViewport this.endRes = al.getWidth() - 1; this.startSeq = 0; this.endSeq = al.getHeight() - 1; + if (applet!=null) + { + // get the width and height scaling factors if they were specified + String param = applet.getParameter("widthScale"); + if (param!=null) + { + try { + widthScale = new Float(param).floatValue(); + } catch (Exception e) + { + } + if (widthScale<=1.0) + { + System.err.println("Invalid alignment character width scaling factor ("+widthScale+"). Ignoring."); + widthScale = 1; + } + if (applet.debug) + { + System.err.println("Alignment character width scaling factor is now "+widthScale); + } + } + param = applet.getParameter("heightScale"); + if (param!=null) + { + try { + heightScale = new Float(param).floatValue(); + } catch (Exception e) + { + } + if (heightScale<=1.0) + { + System.err.println("Invalid alignment character height scaling factor ("+heightScale+"). Ignoring."); + heightScale = 1; + } + if (applet.debug) + { + System.err.println("Alignment character height scaling factor is now "+heightScale); + } + } + } setFont(font); MAC = new jalview.util.Platform().isAMac(); @@ -669,6 +709,8 @@ public class AlignViewport protected FeatureSettings featureSettings = null; + private float heightScale=1,widthScale=1; + public void setFont(Font f) { font = f; @@ -679,14 +721,14 @@ public class AlignViewport } java.awt.FontMetrics fm = nullFrame.getGraphics().getFontMetrics(font); - setCharHeight(fm.getHeight()); - charWidth = fm.charWidth('M'); + setCharHeight((int)(heightScale*fm.getHeight())); + charWidth = (int)(widthScale*fm.charWidth('M')); if (upperCasebold) { Font f2 = new Font(f.getName(), Font.BOLD, f.getSize()); fm = nullFrame.getGraphics().getFontMetrics(f2); - charWidth = fm.stringWidth("MMMMMMMMMMM") / 10; + charWidth = (int)(widthScale*(fm.stringWidth("MMMMMMMMMMM") / 10)); } }