File Source: CustomWindow.java

         /* 
    P/P   *  Method: com.dmdirc.CustomWindow__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;
    24  
    25  import com.dmdirc.config.IdentityManager;
    26  import com.dmdirc.ui.WindowManager;
    27  import com.dmdirc.ui.interfaces.Window;
    28  
    29  /**
    30   * A generic custom window implementation.
    31   *
    32   * @author chris
    33   */
    34  public class CustomWindow extends FrameContainer {
    35  
    36      /** This custom window's name. */
    37      private final String name;
    38  
    39      /** This custom window's title. */
    40      private final String title;
    41  
    42      /** The window used by this container. */
    43      private Window window;
    44  
    45      /** This window's parent window. */
    46      private Window parent;
    47  
    48      /**
    49       * Creates a new custom window as a child of the specified window.
    50       *
    51       * @param name The name of this custom window
    52       * @param title The title of this custom window
    53       * @param parent The parent of this custom window
    54       */
    55      public CustomWindow(final String name, final String title,
    56              final Window parent) {
                 /* 
    P/P           *  Method: void com.dmdirc.CustomWindow(String, String, Window)
                  * 
                  *  Preconditions:
                  *    com/dmdirc/Main.controller != null
                  *    parent != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.ui.interfaces.UIController:getWindow(...)@63 != null
                  *    com.dmdirc.ui.interfaces.Window:getConfigManager(...)@57 != null
                  *    init'ed(com/dmdirc/FrameContainer.java.awt.Color.BLACK)
                  * 
                  *  Postconditions:
                  *    this.changer == &new FrameContainer$IconChanger(FrameContainer#2)
                  *    this.config != null
                  *    this.icon == &"custom"
                  *    this.listeners == &new ListenerList(FrameContainer#1)
                  *    this.name == name
                  *    init'ed(this.name)
                  *    this.notification == com/dmdirc/FrameContainer.java.awt.Color.BLACK
                  *    init'ed(this.notification)
                  *    this.parent == parent
                  *    this.parent != null
                  *    ...
                  */
    57          super("custom", parent.getConfigManager());
    58  
    59          this.name = name;
    60          this.title = title;
    61          this.parent = parent;
    62  
    63          window = Main.getUI().getWindow(this);
    64          window.setTitle(title);
    65  
    66          WindowManager.addWindow(parent, window);
    67  
    68          window.open();
    69      }
    70  
    71      /**
    72       * Creates a new custom window as a top-level window.
    73       *
    74       * @param name The name of this custom window
    75       * @param title The parent of this custom window
    76       */
    77      public CustomWindow(final String name, final String title) {
                 /* 
    P/P           *  Method: void com.dmdirc.CustomWindow(String, String)
                  * 
                  *  Preconditions:
                  *    com/dmdirc/Main.controller != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@78 != null
                  *    com.dmdirc.ui.interfaces.UIController:getWindow(...)@83 != null
                  *    init'ed(com/dmdirc/FrameContainer.java.awt.Color.BLACK)
                  * 
                  *  Postconditions:
                  *    this.changer == &new FrameContainer$IconChanger(FrameContainer#2)
                  *    this.config != null
                  *    this.icon == &"custom"
                  *    this.listeners == &new ListenerList(FrameContainer#1)
                  *    this.name == name
                  *    init'ed(this.name)
                  *    this.notification == com/dmdirc/FrameContainer.java.awt.Color.BLACK
                  *    init'ed(this.notification)
                  *    this.title == title
                  *    init'ed(this.title)
                  *    ...
                  */
    78          super("custom", IdentityManager.getGlobalConfig());
    79  
    80          this.name = name;
    81          this.title = title;
    82  
    83          window = Main.getUI().getWindow(this);
    84          window.setTitle(title);
    85  
    86          WindowManager.addWindow(window);
    87  
    88          window.open();
    89      }
    90  
    91      /** {@inheritDoc} */
    92      @Override
    93      public Window getFrame() {
                 /* 
    P/P           *  Method: Window getFrame()
                  * 
                  *  Preconditions:
                  *    init'ed(this.window)
                  * 
                  *  Postconditions:
                  *    return_value == this.window
                  *    init'ed(return_value)
                  */
    94          return window;
    95      }
    96  
    97      /** {@inheritDoc} */
    98      @Override
    99      public String toString() {
                 /* 
    P/P           *  Method: String toString()
                  * 
                  *  Postconditions:
                  *    return_value == this.name
                  *    init'ed(return_value)
                  */
   100          return name;
   101      }
   102  
   103      /** {@inheritDoc} */
   104      @Override
   105      public void windowClosing() {
   106          // 1: Make the window non-visible
                 /* 
    P/P           *  Method: void windowClosing()
                  * 
                  *  Preconditions:
                  *    this.window != null
                  * 
                  *  Postconditions:
                  *    this.parent == null
                  *    this.window == null
                  */
   107          window.setVisible(false);
   108  
   109          // 2: Remove any callbacks or listeners
   110          // 3: Trigger any actions neccessary
   111          // 4: Trigger action for the window closing
   112          // 5: Inform any parents that the window is closing
   113  
   114          // 6: Remove the window from the window manager
   115          WindowManager.removeWindow(window);
   116  
   117          // 7: Remove any references to the window and parents
   118          window = null; // NOPMD
   119          parent = null; // NOPMD
   120      }
   121  
   122      /** {@inheritDoc} */
   123      @Override
   124      public Server getServer() {
                 /* 
    P/P           *  Method: Server getServer()
                  * 
                  *  Preconditions:
                  *    init'ed(this.parent)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.ui.interfaces.Window:getContainer(...)@125 != null
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   125          return parent == null ? null : parent.getContainer().getServer();
   126      }
   127  
   128      /**
   129       * Retrieves this custom window's name.
   130       *
   131       * @return This custom window's name
   132       */
   133      public String getName() {
                 /* 
    P/P           *  Method: String getName()
                  * 
                  *  Postconditions:
                  *    return_value == this.name
                  *    init'ed(return_value)
                  */
   134          return name;
   135      }
   136  
   137      /**
   138       * Retrieves this custom window's title.
   139       *
   140       * @return This custom window's title
   141       */
   142      public String getTitle() {
                 /* 
    P/P           *  Method: String getTitle()
                  * 
                  *  Postconditions:
                  *    return_value == this.title
                  *    init'ed(return_value)
                  */
   143          return title;
   144      }
   145  
   146  }








SofCheck Inspector Build Version : 2.17854
CustomWindow.java 2009-Jun-25 01:54:24
CustomWindow.class 2009-Sep-02 17:04:12