File Source: HistoryWindow.java

         /* 
    P/P   *  Method: com.dmdirc.addons.logging.HistoryWindow__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.logging;
    24  
    25  import com.dmdirc.FrameContainer;
    26  import com.dmdirc.Main;
    27  import com.dmdirc.Server;
    28  import com.dmdirc.config.IdentityManager;
    29  import com.dmdirc.ui.WindowManager;
    30  import com.dmdirc.ui.interfaces.Window;
    31  
    32  /**
    33   * Displays an extended history of a window.
    34   *
    35   * @author Chris
    36   */
    37  public class HistoryWindow extends FrameContainer {
    38      
    39      /** The title of our window. */
    40      private final String title;
    41         
    42      /** The window we're using. */
    43      private Window window;
    44      
    45      /** Our parent window. */
    46      private Window parent;
    47      
    48      /**
    49       * Creates a new HistoryWindow.
    50       *
    51       * @param title The title of the window
    52       * @param reader The reader to use to get the history
    53       * @param parent The window this history window was opened from
    54       * @param numLines The number of lines to show
    55       */
    56      public HistoryWindow(final String title, final ReverseFileReader reader, 
    57              final Window parent, final int numLines) {
                 /* 
    P/P           *  Method: void com.dmdirc.addons.logging.HistoryWindow(String, ReverseFileReader, Window, int)
                  * 
                  *  Preconditions:
                  *    parent != null
                  *    reader != null
                  *    (soft) reader.file != null
                  *    (soft) init'ed(reader.seekLength)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.Main:getUI(...)@62 != null
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@67 != null
                  *    com.dmdirc.ui.interfaces.UIController:getWindow(...)@62 != null
                  * 
                  *  Postconditions:
                  *    this.parent == parent
                  *    this.parent != null
                  *    this.title == title
                  *    init'ed(this.title)
                  *    this.window != null
                  */
    58          super("raw", parent.getConfigManager());
    59          this.title = title;
    60          this.parent = parent;
    61          
    62          window = Main.getUI().getWindow(this);
    63          
    64          WindowManager.addWindow(parent, window);
    65          window.setTitle(title);
    66          window.open();
    67          final int frameBufferSize = IdentityManager.getGlobalConfig().getOptionInt(
    68                  "ui", "frameBufferSize");
    69          window.addLine(reader.getLinesAsString(Math.min(frameBufferSize, numLines)), false);
    70      }
    71      
    72      /** {@inheritDoc} */
    73      @Override
    74      public Window getFrame() {
                 /* 
    P/P           *  Method: Window getFrame()
                  * 
                  *  Preconditions:
                  *    init'ed(this.window)
                  * 
                  *  Postconditions:
                  *    return_value == this.window
                  *    init'ed(return_value)
                  */
    75          return window;
    76      }
    77      
    78      /** {@inheritDoc} */
    79      @Override
    80      public String toString() {
                 /* 
    P/P           *  Method: String toString()
                  * 
                  *  Postconditions:
                  *    return_value == this.title
                  *    init'ed(return_value)
                  */
    81          return title;
    82      }
    83      
    84      /** {@inheritDoc} */
    85      @Override
    86      public void windowClosing() {
    87          // 1: Make the window non-visible
                 /* 
    P/P           *  Method: void windowClosing()
                  * 
                  *  Preconditions:
                  *    this.window != null
                  * 
                  *  Postconditions:
                  *    this.parent == null
                  *    this.window == null
                  */
    88          window.setVisible(false);
    89          
    90          // 2: Remove any callbacks or listeners
    91          // 3: Trigger any actions neccessary
    92          // 4: Trigger action for the window closing
    93          // 5: Inform any parents that the window is closing
    94          
    95          // 6: Remove the window from the window manager
    96          WindowManager.removeWindow(window);
    97          
    98          // 7: Remove any references to the window and parents
    99          window = null; // NOPMD
   100          parent = null; // NOPMD
   101      }
   102      
   103      /** {@inheritDoc} */
   104      @Override
   105      public Server getServer() {
                 /* 
    P/P           *  Method: Server getServer()
                  * 
                  *  Preconditions:
                  *    init'ed(this.parent)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.ui.interfaces.Window:getContainer(...)@106 != null
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   106          return parent == null ? null : parent.getContainer().getServer();
   107      }
   108  
   109  }








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