new applet parameters: heightScale and widthScale

diff --git a/src/jalview/appletgui/AlignViewport.java b/src/jalview/appletgui/AlignViewport.java
index 684e005..8e80376 100755 (executable)
--- 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));
     }
   }