File Source: WindowManager.java

         /* 
    P/P   *  Method: com.dmdirc.ui.WindowManager$WMSelectionListener__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.ui;
    24  
    25  import com.dmdirc.CustomWindow;
    26  import com.dmdirc.Precondition;
    27  import com.dmdirc.interfaces.SelectionListener;
    28  import com.dmdirc.logger.ErrorLevel;
    29  import com.dmdirc.logger.Logger;
    30  import com.dmdirc.ui.interfaces.FrameManager;
    31  import com.dmdirc.ui.interfaces.Window;
    32  import com.dmdirc.util.MapList;
    33  
    34  import java.util.ArrayList;
    35  import java.util.List;
    36  import java.util.Map.Entry;
    37  
    38  /**
    39   * The WindowManager maintains a list of all open windows, and their
    40   * parent/child relations.
    41   *
    42   * @author Chris
    43   */
         /* 
    P/P   *  Method: List access$100()
          * 
          *  Postconditions:
          *    return_value == &new ArrayList(WindowManager__static_init#4)
          */
    44  public class WindowManager {
    45  
    46      /** A list of root windows. */
             /* 
    P/P       *  Method: com.dmdirc.ui.WindowManager__static_init
              * 
              *  Postconditions:
              *    childWindows == &new MapList(WindowManager__static_init#2)
              *    frameManagers == &new ArrayList(WindowManager__static_init#3)
              *    rootWindows == &new ArrayList(WindowManager__static_init#1)
              *    selListeners == &new ArrayList(WindowManager__static_init#4)
              *    selectionListener == &new WindowManager$WMSelectionListener(WindowManager__static_init#5)
              *    new ArrayList(WindowManager__static_init#1) num objects == 1
              *    new ArrayList(WindowManager__static_init#3) num objects == 1
              *    new ArrayList(WindowManager__static_init#4) num objects == 1
              *    new MapList(WindowManager__static_init#2) num objects == 1
              *    new WindowManager$WMSelectionListener(WindowManager__static_init#5) num objects == 1
              */
    47      private final static List<Window> rootWindows
    48              = new ArrayList<Window>();
    49  
    50      /** A map of parent windows to their children. */
    51      private final static MapList<Window, Window> childWindows
    52              = new MapList<Window, Window>();
    53  
    54      /** A list of frame managers. */
    55      private final static List<FrameManager> frameManagers
    56              = new ArrayList<FrameManager>();
    57      
    58      /** A list of selection listeners. */
    59      private final static List<SelectionListener> selListeners
    60              = new ArrayList<SelectionListener>();
    61      
    62      /** Our selection listener proxy. */
    63      private static final SelectionListener selectionListener
    64              = new WMSelectionListener();
    65  
    66      /**
    67       * Creates a new instance of WindowManager.
    68       */
             /* 
    P/P       *  Method: void com.dmdirc.ui.WindowManager()
              */
    69      private WindowManager() {
    70          // Shouldn't be instansiated
    71      }
    72  
    73      /**
    74       * Registers a FrameManager with the WindowManager.
    75       *
    76       * @param frameManager The frame manager to be registered
    77       */
    78      @Precondition({
    79          "The specified FrameManager is not null",
    80          "The specified FrameManager has not already been added"
    81      })
    82      public static void addFrameManager(final FrameManager frameManager) {
                 /* 
    P/P           *  Method: void addFrameManager(FrameManager)
                  */
    83          Logger.assertTrue(frameManager != null);
    84          Logger.assertTrue(!frameManagers.contains(frameManager));
    85  
    86          frameManagers.add(frameManager);
    87      }
    88  
    89      /**
    90       * Unregisters a FrameManager with the WindowManager.
    91       *
    92       * @param frameManager The frame manager to be removed
    93       */
    94      @Precondition({
    95          "The specified FrameManager is not null",
    96          "The specified FrameManager has already been added and not removed"
    97      })
    98      public static void removeFrameManager(final FrameManager frameManager) {
                 /* 
    P/P           *  Method: void removeFrameManager(FrameManager)
                  * 
                  *  Presumptions:
                  *    java.util.List:contains(...)@100 == 1
                  */
    99          Logger.assertTrue(frameManager != null);
   100          Logger.assertTrue(frameManagers.contains(frameManager));
   101  
   102          frameManagers.remove(frameManager);
   103      }
   104      
   105      /**
   106       * Registers the specified SelectionListener with the WindowManager.
   107       * 
   108       * @param listener The listener to be added
   109       */
   110      public static void addSelectionListener(final SelectionListener listener) {
                 /* 
    P/P           *  Method: void addSelectionListener(SelectionListener)
                  */
   111          selListeners.add(listener);
   112      }
   113      
   114      /**
   115       * Unregisters the specified SelectionListener with the WindowManager.
   116       * 
   117       * @param listener The listener to be removed
   118       */
   119      public static void removeSelectionListener(final SelectionListener listener) {
                 /* 
    P/P           *  Method: void removeSelectionListener(SelectionListener)
                  */
   120          selListeners.remove(listener);
   121      }
   122  
   123      /**
   124       * Adds a new root window to the Window Manager.
   125       *
   126       * @param window The window to be added
   127       */
   128      @Precondition({
   129          "The specified Window is not null",
   130          "The specified Window has not already been added"
   131      })
   132      public static void addWindow(final Window window) {
                 /* 
    P/P           *  Method: void addWindow(Window)
                  * 
                  *  Preconditions:
                  *    window != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.ui.interfaces.Window:getContainer(...)@139 != null
                  */
   133          Logger.assertTrue(window != null);
   134          Logger.assertTrue(!rootWindows.contains(window));
   135  
   136          rootWindows.add(window);
   137          childWindows.add(window);
   138          
   139          window.getContainer().addSelectionListener(selectionListener);
   140  
   141          fireAddWindow(window);
   142      }
   143  
   144      /**
   145       * Adds a new child window to the Window Manager.
   146       *
   147       * @param parent The parent window
   148       * @param child The child window to be added
   149       */
   150      @Precondition({
   151          "The specified Windows are not null",
   152          "The parent Window has already been added",
   153          "The child Window has not already been added"
   154      })
   155      public static void addWindow(final Window parent, final Window child) {
                 /* 
    P/P           *  Method: void addWindow(Window, Window)
                  * 
                  *  Preconditions:
                  *    child != null
                  *    (soft) parent != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.ui.interfaces.Window:getContainer(...)@164 != null
                  *    com.dmdirc.util.MapList:containsKey(...)@158 == 1
                  */
   156          Logger.assertTrue(parent != null);
   157          Logger.assertTrue(child != null);
   158          Logger.assertTrue(childWindows.containsKey(parent));
   159          Logger.assertTrue(!childWindows.containsKey(child));
   160  
   161          childWindows.add(parent, child);
   162          childWindows.add(child);
   163          
   164          child.getContainer().addSelectionListener(selectionListener);
   165  
   166          fireAddWindow(parent, child);
   167      }
   168  
   169      /**
   170       * Removes a window from the Window Manager. If the specified window
   171       * has child windows, they are recursively removed before the target window.
   172       * If the window hasn't previously been added, the reques to remove it is
   173       * ignored.
   174       *
   175       * @param window The window to be removed
   176       */
   177      @Precondition("The specified Window is not null")
   178      public static void removeWindow(final Window window) {
                 /* 
    P/P           *  Method: void removeWindow(Window)
                  * 
                  *  Preconditions:
                  *    (soft) com.dmdirc.logger.ErrorManager__static_init.new Class[](ErrorManager__static_init#2)[...] != null
                  *    (soft) init'ed(com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).logReports)
                  *    (soft) com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).nextErrorID != null
                  *    (soft) init'ed(com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).sendReports)
                  *    (soft) init'ed(com.dmdirc.ui.FatalErrorDialog$4__static_init.new int[](FatalErrorDialog$4__static_init#1)[...])
                  *    (soft) init'ed(com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).reportThread)
                  *    (soft) init'ed(com/dmdirc/logger/ProgramError.errorDir)
                  *    (soft) window != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.logger.ErrorManager__static_init.new Class[](ErrorManager__static_init#2)[...]@193 != null
                  *    com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).nextErrorID@193 != null
                  *    com.dmdirc.ui.interfaces.Window:getContainer(...)@228 != null
                  *    com.dmdirc.util.MapList:get(...)@185 != null
                  *    com.dmdirc.util.MapList:get(...)@190 != null
                  *    ...
                  * 
                  *  Postconditions:
                  *    init'ed(com/dmdirc/logger/ProgramError.errorDir)
                  *    init'ed(com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).reportThread)
                  *    new ErrorReportingThread(sendError#1) num objects <= 1
                  *    init'ed(new ErrorReportingThread(sendError#1).queue)
                  *    new File(getErrorFile#1) num objects <= 1
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.util.MapList:containsKey(...)@181: {1}, {0}
                  *    com.dmdirc.util.MapList:get(...)@185: Addr_Set{null}, Inverse{null}
                  *    java.util.Iterator:hasNext(...)@186: {0}, {1}
                  *    java.util.List:contains(...)@205: {0}, {1}
                  *    java.util.List:isEmpty(...)@185: {1}, {0}
                  *    java.util.List:isEmpty(...)@190: {1}, {0}
                  */
   179          Logger.assertTrue(window != null);
   180          
   181          if (!childWindows.containsKey(window)) {
   182              return;
   183          }
   184  
   185          if (childWindows.get(window) != null && !childWindows.get(window).isEmpty()) {
   186              for (Window child : new ArrayList<Window>(childWindows.get(window))) {
   187                  child.close();
   188              }
   189  
   190              while (!childWindows.get(window).isEmpty()) {
   191                  try {
   192                      synchronized (childWindows) {
   193                          childWindows.wait();
   194                      }
   195                  } catch (InterruptedException ex) {
   196                      // Ignore it
   197                  }
   198              }
   199          }
   200  
   201          synchronized (childWindows) {
   202              childWindows.remove(window);
   203          }
   204  
   205          if (rootWindows.contains(window)) {
   206              rootWindows.remove(window);
   207  
   208              fireDeleteWindow(window);
   209          } else {
   210              final Window parent = getParent(window);
   211  
   212              if (parent == null) {
   213                  Logger.appError(ErrorLevel.MEDIUM, "Invalid window removed",
   214                          new IllegalArgumentException("Tried to remove a" +
   215                          " non-root window that has no known parent.\nWindow:" +
   216                          " " + window.getTitle()));
   217                  return;
   218              } else {
   219                  synchronized (childWindows) {
   220                      childWindows.remove(parent, window);
   221                      childWindows.notifyAll();
   222                  }
   223  
   224                  fireDeleteWindow(parent, window);
   225              }
   226          }
   227          
   228          window.getContainer().removeSelectionListener(selectionListener);
   229      }
   230  
   231      /**
   232       * Finds and returns a global custom window with the specified name.
   233       * If a custom window with the specified name isn't found, null is returned.
   234       * 
   235       * @param name The name of the custom window to search for
   236       * @return The specified custom window, or null
   237       */
   238      @Precondition("The specified window name is not null")
   239      public static Window findCustomWindow(final String name) {
                 /* 
    P/P           *  Method: Window findCustomWindow(String)
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   240          Logger.assertTrue(name != null);
   241  
   242          return findCustomWindow(rootWindows, name);
   243      }
   244  
   245      /**
   246       * Finds and returns a non-global custom window with the specified name.
   247       * If a custom window with the specified name isn't found, null is returned.
   248       * 
   249       * @param parent The parent whose children should be searched
   250       * @param name The name of the custom window to search for
   251       * @return The specified custom window, or null
   252       */
   253      @Precondition({
   254          "The specified window name is not null",
   255          "The specified parent window is not null",
   256          "The specified parent window has been added to the Window Manager"
   257      })
   258      public static Window findCustomWindow(final Window parent, final String name) {
                 /* 
    P/P           *  Method: Window findCustomWindow(Window, String)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.util.MapList:containsKey(...)@261 == 1
                  *    com.dmdirc.util.MapList:get(...)@263 != null
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   259          Logger.assertTrue(parent != null);
   260          Logger.assertTrue(name != null);
   261          Logger.assertTrue(childWindows.containsKey(parent));
   262  
   263          return findCustomWindow(childWindows.get(parent), name);
   264      }
   265  
   266      /**
   267       * Finds a custom window with the specified name among the specified list
   268       * of windows. If the custom window is not found, returns null.
   269       * 
   270       * @param windows The list of windows to search
   271       * @param name The name of the custom window to search for
   272       * @return The custom window if found, or null otherwise
   273       */
   274      private static Window findCustomWindow(final List<Window> windows, final String name) {
                 /* 
    P/P           *  Method: Window findCustomWindow(List, String)
                  * 
                  *  Preconditions:
                  *    windows != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.CustomWindow:getName(...)@276 != null
                  *    com.dmdirc.ui.interfaces.Window:getContainer(...)@276 != null
                  *    java.util.Iterator:next(...)@275 != null
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  * 
                  *  Test Vectors:
                  *    java.lang.String:equals(...)@276: {0}, {1}
                  *    java.util.Iterator:hasNext(...)@275: {0}, {1}
                  */
   275          for (Window window : windows) {
   276              if (window.getContainer() instanceof CustomWindow
   277                      && ((CustomWindow) window.getContainer()).getName().equals(name)) {
   278                  return window;
   279              }
   280          }
   281  
   282          return null;
   283      }
   284  
   285      /**
   286       * Retrieves the parent window of the specified window. If the window
   287       * has no parent (i.e., it is a root window or it has not been added),
   288       * returns null.
   289       * 
   290       * @param window The window whose parent is being sought
   291       * @return The parent of the specified window, or null if not found
   292       */
   293      public static Window getParent(final Window window) {
                 /* 
    P/P           *  Method: Window getParent(Window)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.util.MapList:entrySet(...)@295 != null
                  *    java.util.Iterator:next(...)@295 != null
                  *    java.util.Map_Entry:getValue(...)@296 != null
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  * 
                  *  Test Vectors:
                  *    java.util.Iterator:hasNext(...)@295: {1}, {0}
                  *    java.util.List:contains(...)@296: {0}, {1}
                  */
   294          synchronized (childWindows) {
   295              for (Entry<Window, List<Window>> entry : childWindows.entrySet()) {
   296                  if (entry.getValue().contains(window)) {
   297                      return entry.getKey();
   298                  }
   299              }
   300          }
   301  
   302          return null;
   303      }
   304      
   305      /**
   306       * Retrieves all known root (parent-less) windows.
   307       * 
   308       * @since 0.6
   309       * @return An array of all known root windows.
   310       */
   311      public static Window[] getRootWindows() {
                 /* 
    P/P           *  Method: Window[] getRootWindows()
                  * 
                  *  Presumptions:
                  *    java.util.List:size(...)@312 >= 0
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   312          return rootWindows.toArray(new Window[rootWindows.size()]);
   313      }
   314      
   315      /**
   316       * Retrieves all children of the specified window.
   317       * 
   318       * @since 0.6
   319       * @param window The window whose children are being requested
   320       * @return An array of all known child windows.
   321       */
   322      public static Window[] getChildren(final Window window) {
                 /* 
    P/P           *  Method: Window[] getChildren(Window)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.util.MapList:get(...)@323 != null
                  *    java.util.List:size(...)@324 >= 0
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   323          final List<Window> children = childWindows.get(window);
   324          return children.toArray(new Window[children.size()]);
   325      }
   326      
   327      /**
   328       * Fires the addWindow(Window) callback.
   329       * 
   330       * @param window The window that was added
   331       */
   332      private static void fireAddWindow(final Window window) {
                 /* 
    P/P           *  Method: void fireAddWindow(Window)
                  * 
                  *  Preconditions:
                  *    (soft) window != null
                  * 
                  *  Presumptions:
                  *    java.util.Iterator:next(...)@333 != null
                  * 
                  *  Test Vectors:
                  *    java.util.Iterator:hasNext(...)@333: {0}, {1}
                  */
   333          for (FrameManager manager : frameManagers) {
   334              manager.addWindow(window.getContainer());
   335          }
   336      }
   337  
   338      /**
   339       * Fires the addWindow(Window, Window) callback.
   340       * 
   341       * @param parent The parent window
   342       * @param child The new child window that was added
   343       */
   344      private static void fireAddWindow(final Window parent, final Window child) {
                 /* 
    P/P           *  Method: void fireAddWindow(Window, Window)
                  * 
                  *  Preconditions:
                  *    (soft) child != null
                  *    (soft) parent != null
                  * 
                  *  Presumptions:
                  *    java.util.Iterator:next(...)@345 != null
                  * 
                  *  Test Vectors:
                  *    java.util.Iterator:hasNext(...)@345: {0}, {1}
                  */
   345          for (FrameManager manager : frameManagers) {
   346              manager.addWindow(parent.getContainer(), child.getContainer());
   347          }
   348      }
   349  
   350      /**
   351       * Fires the delWindow(Window) callback.
   352       * 
   353       * @param window The window that was removed
   354       */
   355      private static void fireDeleteWindow(final Window window) {
                 /* 
    P/P           *  Method: void fireDeleteWindow(Window)
                  * 
                  *  Preconditions:
                  *    (soft) window != null
                  * 
                  *  Presumptions:
                  *    java.util.Iterator:next(...)@356 != null
                  * 
                  *  Test Vectors:
                  *    java.util.Iterator:hasNext(...)@356: {0}, {1}
                  */
   356          for (FrameManager manager : frameManagers) {
   357              manager.delWindow(window.getContainer());
   358          }
   359      }
   360  
   361      /**
   362       * Fires the delWindow(Window, Window) callback.
   363       * 
   364       * @param parent The parent window
   365       * @param child The child window that was removed
   366       */
   367      private static void fireDeleteWindow(final Window parent, final Window child) {
                 /* 
    P/P           *  Method: void fireDeleteWindow(Window, Window)
                  * 
                  *  Preconditions:
                  *    (soft) child != null
                  *    (soft) parent != null
                  * 
                  *  Presumptions:
                  *    java.util.Iterator:next(...)@368 != null
                  * 
                  *  Test Vectors:
                  *    java.util.Iterator:hasNext(...)@368: {0}, {1}
                  */
   368          for (FrameManager manager : frameManagers) {
   369              manager.delWindow(parent.getContainer(), child.getContainer());
   370          }
   371      }
   372          
   373      /**
   374       * Proxy for selection events.
   375       */
             /* 
    P/P       *  Method: void com.dmdirc.ui.WindowManager$WMSelectionListener(WindowManager$1)
              */
   376      private static class WMSelectionListener implements SelectionListener {
   377  
   378          /** {@inheritDoc} */
   379          @Override
   380          public void selectionChanged(final Window window) {
                     /* 
    P/P               *  Method: void selectionChanged(Window)
                      * 
                      *  Presumptions:
                      *    java.util.Iterator:next(...)@381 != null
                      * 
                      *  Test Vectors:
                      *    java.util.Iterator:hasNext(...)@381: {0}, {1}
                      */
   381              for (SelectionListener listener : selListeners) {
   382                  listener.selectionChanged(window);
   383              }
   384          }
   385          
   386      }
   387  
   388  }








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