Font increase/decrease feature in GUI.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@486 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/userinterface/GUIPrism.java

@@ -33,6 +33,7 @@ import java.net.*;
 import java.awt.*;
 import java.awt.event.*;
 import javax.swing.*;
+import javax.swing.plaf.*;
 import javax.swing.plaf.metal.*;
 //Prism Packages
 import prism.*;
@@ -70,6 +71,23 @@ public class GUIPrism extends JFrame
     private static GUIPrism gui;
     private boolean doExit;
     
+    
+    public void adjustFont( int adjust )
+    {
+        Object[] objs = UIManager.getLookAndFeel().getDefaults().keySet().toArray();
+        for( int i = 0; i < objs.length; i++ )
+        {
+            if( objs[i].toString().toUpperCase().indexOf( ".FONT" ) != -1 )
+            {
+                Font font = UIManager.getFont( objs[i] );
+                font = font.deriveFont( (float)(font.getSize() + adjust ));
+                UIManager.put( objs[i], new FontUIResource(font) );
+            }
+        }
+        SwingUtilities.updateComponentTreeUI(this);
+        repaint();
+    }
+    
     //STATIC METHODS
     
     /** The entry point of the program from the command line.
@@ -141,6 +159,8 @@ public class GUIPrism extends JFrame
     private JProgressBar progress;
     private GUITaskBar taskbar;
     private Action prismOptions;
+    private Action fontIncrease;
+    private Action fontDecrease;
     
     //CONSTRUCTORS AND INITIALISATION METHODS
     
@@ -286,6 +306,38 @@ public class GUIPrism extends JFrame
         optionsMenu.add(prismOptions);
         optionsMenu.setMnemonic('O');
         
+        fontIncrease = new AbstractAction()
+        {
+            public void actionPerformed(ActionEvent e)
+            {
+                adjustFont(1);
+            }
+        };
+        fontIncrease.putValue(Action.LONG_DESCRIPTION, "Increase the application font size.");
+        fontIncrease.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_I));
+        fontIncrease.putValue(Action.NAME, "Increase font size");
+        fontIncrease.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFontIncrease.png"));
+		fontIncrease.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_EQUALS, InputEvent.CTRL_MASK | InputEvent.SHIFT_MASK));
+        
+        optionsMenu.add(fontIncrease);
+        optionsMenu.setMnemonic('I');
+        
+        fontDecrease = new AbstractAction()
+        {
+            public void actionPerformed(ActionEvent e)
+            {
+                adjustFont(-1);
+            }
+        };
+        fontDecrease.putValue(Action.LONG_DESCRIPTION, "Decrease the application font size.");
+        fontDecrease.putValue(Action.MNEMONIC_KEY, new Integer(KeyEvent.VK_D));
+        fontDecrease.putValue(Action.NAME, "Decrease font size");
+        fontDecrease.putValue(Action.SMALL_ICON, GUIPrism.getIconFromImage("smallFontDecrease.png"));
+		fontDecrease.putValue(Action.ACCELERATOR_KEY, KeyStroke.getKeyStroke(KeyEvent.VK_MINUS, InputEvent.CTRL_MASK));
+        
+        optionsMenu.add(fontDecrease);
+        optionsMenu.setMnemonic('D');
+        
         JPanel bottomPanel = new JPanel();
         {
             progress = new JProgressBar(0,100);