From e8b96bbe1b40aa5facf4b57df77920c763f5c87d Mon Sep 17 00:00:00 2001
From: Dave Parker <dave.x.parker@gmail.com>
Date: Fri, 26 Oct 2007 16:48:40 +0000
Subject: [PATCH] Code tidy for font increase/decrease feature in GUI.

git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@487 bbc10eb1-c90d-0410-af57-cb519fbb1720
---
 prism/src/userinterface/GUIPrism.java | 36 +++++++++++++++------------
 1 file changed, 20 insertions(+), 16 deletions(-)

diff --git a/prism/src/userinterface/GUIPrism.java b/prism/src/userinterface/GUIPrism.java
index c185fd8c..298f6ebb 100644
--- a/prism/src/userinterface/GUIPrism.java
+++ b/prism/src/userinterface/GUIPrism.java
@@ -72,22 +72,6 @@ public class GUIPrism extends JFrame
     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.
@@ -378,6 +362,26 @@ public class GUIPrism extends JFrame
         }
     }
     
+    /**
+     *  Adjust the main font for the GUI (+1 = one size up, -1 = one size down)
+     */
+	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();
+    }
+    
+
     //EXITERS
     public void exit()
     {