File Source: FrameContainerMenuItem.java

         /* 
    P/P   *  Method: com.dmdirc.addons.ui_swing.framemanager.windowmenu.FrameContainerMenuItem__static_init
          */
     1  /*
     2   * Copyright (c) 2006-2009 Chris Smith, Shane Mc Cormack, Gregory Holmes
     3   * 
     4   * Permission is hereby granted, free of charge, to any person obtaining a copy
     5   * of this software and associated documentation files (the "Software"), to deal
     6   * in the Software without restriction, including without limitation the rights
     7   * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
     8   * copies of the Software, and to permit persons to whom the Software is
     9   * furnished to do so, subject to the following conditions:
    10   * 
    11   * The above copyright notice and this permission notice shall be included in
    12   * all copies or substantial portions of the Software.
    13   * 
    14   * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
    15   * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
    16   * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
    17   * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
    18   * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
    19   * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
    20   * SOFTWARE.
    21   */
    22  
    23  package com.dmdirc.addons.ui_swing.framemanager.windowmenu;
    24  
    25  import com.dmdirc.FrameContainer;
    26  import com.dmdirc.interfaces.IconChangeListener;
    27  import com.dmdirc.ui.interfaces.Window;
    28  
    29  import java.awt.Font;
    30  import java.awt.event.ActionEvent;
    31  import java.awt.event.ActionListener;
    32  import javax.swing.Icon;
    33  import javax.swing.JMenuItem;
    34  import javax.swing.SwingUtilities;
    35  
    36  /**
    37   * Action representing a frame.
    38   */
         /* 
    P/P   *  Method: FrameContainer access$000(FrameContainerMenuItem)
          * 
          *  Preconditions:
          *    x0 != null
          *    init'ed(x0.frame)
          * 
          *  Postconditions:
          *    return_value == x0.frame
          *    init'ed(return_value)
          */
    39  public class FrameContainerMenuItem extends JMenuItem implements IconChangeListener,
    40          ActionListener {
    41  
    42      /**
    43       * A version number for this class. It should be changed whenever the class
    44       * structure is changed (or anything else that would prevent serialized
    45       * objects being unserialized with the new class).
    46       */
    47      private static final long serialVersionUID = 1;
    48      /** Wrapped frame. */
    49      private FrameContainer frame;
    50  
    51      /**
    52       * Instantiates a new FrameContainer menu item wrapping the specified frame.
    53       * 
    54       * @param frame Wrapped frame
    55       */
    56      public FrameContainerMenuItem(final FrameContainer frame) {
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.framemanager.windowmenu.FrameContainerMenuItem(FrameContainer)
                  * 
                  *  Preconditions:
                  *    frame != null
                  * 
                  *  Postconditions:
                  *    this.frame == frame
                  *    this.frame != null
                  */
    57          super(frame.toString(), frame.getIcon());
    58  
    59          this.frame = frame;
    60  
    61          addActionListener(this);
    62          frame.addIconChangeListener(this);
    63      }
    64  
    65      /** {@inheritDoc} */
    66      @Override
    67      public void iconChanged(final Window window, final Icon icon) {
                 /* 
    P/P           *  Method: void iconChanged(Window, Icon)
                  */
    68          SwingUtilities.invokeLater(new Runnable() {
    69  
    70              /** {@inheritDoc} */
    71              @Override
    72              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    init'ed(this.frame)
                          * 
                          *  Test Vectors:
                          *    this.frame: Addr_Set{null}, Inverse{null}
                          *    this.val$window: Addr_Set{null}, Inverse{null}
                          *    java.lang.Object:equals(...)@73: {0}, {1}
                          */
    73                  if ((frame != null && window != null) &&
    74                          frame.equals(window.getContainer())) {
    75                      setIcon(icon);
    76                  }
    77              }
    78          });
    79      }
    80  
    81      /** 
    82       * {@inheritDoc}
    83       * 
    84       * @param e Action event
    85       */
    86      @Override
    87      public void actionPerformed(final ActionEvent e) {
                 /* 
    P/P           *  Method: void actionPerformed(ActionEvent)
                  * 
                  *  Preconditions:
                  *    this.frame != null
                  */
    88          frame.activateFrame();
    89      }
    90  
    91      /**
    92       * Called when a new window is selected.
    93       *
    94       * @param window The window that's now selected
    95       */
    96      public void selectionChanged(final Window window) {
                 /* 
    P/P           *  Method: void selectionChanged(Window)
                  * 
                  *  Preconditions:
                  *    this.frame != null
                  *    window != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.addons.ui_swing.framemanager.windowmenu.FrameContainerMenuItem:getFont(...)@100 != null
                  *    com.dmdirc.addons.ui_swing.framemanager.windowmenu.FrameContainerMenuItem:getFont(...)@98 != null
                  * 
                  *  Test Vectors:
                  *    java.lang.Object:equals(...)@97: {0}, {1}
                  */
    97          if (frame.equals(window.getContainer())) {
    98              setFont(getFont().deriveFont(Font.BOLD));
    99          } else {
   100              setFont(getFont().deriveFont(Font.PLAIN));
   101          }
   102      }
   103  
   104      /**
   105       * Returns the wrapped frame container.
   106       * 
   107       * @return Wrapped frame container
   108       */
   109      public FrameContainer getFrame() {
                 /* 
    P/P           *  Method: FrameContainer getFrame()
                  * 
                  *  Preconditions:
                  *    init'ed(this.frame)
                  * 
                  *  Postconditions:
                  *    return_value == this.frame
                  *    init'ed(return_value)
                  */
   110          return frame;
   111      }
   112  }








SofCheck Inspector Build Version : 2.17854
FrameContainerMenuItem.java 2009-Jun-25 01:54:24
FrameContainerMenuItem.class 2009-Sep-02 17:04:16
FrameContainerMenuItem$1.class 2009-Sep-02 17:04:16