diff options
| author | Matthias Schiffer <mschiffer@universe-factory.net> | 2011-06-08 21:58:16 +0200 |
|---|---|---|
| committer | Matthias Schiffer <mschiffer@universe-factory.net> | 2011-06-08 21:58:16 +0200 |
| commit | 45d5b3ae10ed8cfbecb5489636093c6fb0576970 (patch) | |
| tree | 1aa1c012f46fe204d997e8c6896940800f5461bb /src/jrummikub/view/impl/WinPanel.java | |
| parent | 2e376414b941da3c6fa3c20ddad085c695175542 (diff) | |
| download | JRummikub-45d5b3ae10ed8cfbecb5489636093c6fb0576970.tar JRummikub-45d5b3ae10ed8cfbecb5489636093c6fb0576970.zip | |
Implement pause function
git-svn-id: svn://sunsvr01.isp.uni-luebeck.de/swproj13/trunk@390 72836036-5685-4462-b002-a69064685172
Diffstat (limited to 'src/jrummikub/view/impl/WinPanel.java')
| -rw-r--r-- | src/jrummikub/view/impl/WinPanel.java | 10 |
1 files changed, 4 insertions, 6 deletions
diff --git a/src/jrummikub/view/impl/WinPanel.java b/src/jrummikub/view/impl/WinPanel.java index ff6f68a..2134a8e 100644 --- a/src/jrummikub/view/impl/WinPanel.java +++ b/src/jrummikub/view/impl/WinPanel.java @@ -101,8 +101,7 @@ class WinPanel extends JPanel { private void rescale() { Insets insets = getInsets(); int x = insets.left, y = insets.top, width = getWidth() - insets.left - - insets.right, height = getHeight() - insets.top - - insets.bottom; + - insets.right, height = getHeight() - insets.top - insets.bottom; if (width > PANEL_MAX_WIDTH) { x += (width - PANEL_MAX_WIDTH) / 4; @@ -118,14 +117,13 @@ class WinPanel extends JPanel { newRoundButton.setBounds(x, y, buttonWidth, buttonHeight); newRoundButton.setFont(newRoundButton.getFont().deriveFont(fontSize)); - newGameButton.setBounds(x + buttonWidth + PANEL_SEPARATOR, y, - buttonWidth, buttonHeight); + newGameButton.setBounds(x + buttonWidth + PANEL_SEPARATOR, y, buttonWidth, + buttonHeight); newGameButton.setFont(newGameButton.getFont().deriveFont(fontSize)); endProgramButton.setBounds(x + 2 * (buttonWidth + PANEL_SEPARATOR), y, buttonWidth, buttonHeight); - endProgramButton.setFont(endProgramButton.getFont() - .deriveFont(fontSize)); + endProgramButton.setFont(endProgramButton.getFont().deriveFont(fontSize)); } } |