//# 8 errors, 437 messages
//#
/*
    //#WindowManager.java:1:1: class: com.dmdirc.ui.WindowManager
    //#WindowManager.java:1:1: class: com.dmdirc.ui.WindowManager$1
    //#WindowManager.java:1:1: method: com.dmdirc.ui.WindowManager$1.com.dmdirc.ui.WindowManager$1__static_init
    //#WindowManager.java:1:1: class: com.dmdirc.ui.WindowManager$WMSelectionListener
    //#WindowManager.java:1:1: method: com.dmdirc.ui.WindowManager$WMSelectionListener.com.dmdirc.ui.WindowManager$WMSelectionListener__static_init
 * Copyright (c) 2006-2009 Chris Smith, Shane Mc Cormack, Gregory Holmes
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
 * copies of the Software, and to permit persons to whom the Software is
 * furnished to do so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be included in
 * all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
 * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
 * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
 * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
 * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
 * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
 * SOFTWARE.
 */

package com.dmdirc.ui;

import com.dmdirc.CustomWindow;
import com.dmdirc.Precondition;
import com.dmdirc.interfaces.SelectionListener;
import com.dmdirc.logger.ErrorLevel;
import com.dmdirc.logger.Logger;
import com.dmdirc.ui.interfaces.FrameManager;
import com.dmdirc.ui.interfaces.Window;
import com.dmdirc.util.MapList;

import java.util.ArrayList;
import java.util.List;
import java.util.Map.Entry;

/**
 * The WindowManager maintains a list of all open windows, and their
 * parent/child relations.
 *
 * @author Chris
 */
public class WindowManager {
    //#WindowManager.java:44: method: List com.dmdirc.ui.WindowManager.access$100()
    //#input(List access$100()): selListeners
    //#output(List access$100()): return_value
    //#post(List access$100()): return_value == &new ArrayList(WindowManager__static_init#4)
    //#WindowManager.java:44: end of method: List com.dmdirc.ui.WindowManager.access$100()

    /** A list of root windows. */
    private final static List<Window> rootWindows
    //#WindowManager.java:47: method: com.dmdirc.ui.WindowManager.com.dmdirc.ui.WindowManager__static_init
    //#output(com.dmdirc.ui.WindowManager__static_init): __Descendant_Table[com/dmdirc/ui/WindowManager]
    //#output(com.dmdirc.ui.WindowManager__static_init): childWindows
    //#output(com.dmdirc.ui.WindowManager__static_init): frameManagers
    //#output(com.dmdirc.ui.WindowManager__static_init): new ArrayList(WindowManager__static_init#1) num objects
    //#output(com.dmdirc.ui.WindowManager__static_init): new ArrayList(WindowManager__static_init#3) num objects
    //#output(com.dmdirc.ui.WindowManager__static_init): new ArrayList(WindowManager__static_init#4) num objects
    //#output(com.dmdirc.ui.WindowManager__static_init): new MapList(WindowManager__static_init#2) num objects
    //#output(com.dmdirc.ui.WindowManager__static_init): new WindowManager$WMSelectionListener(WindowManager__static_init#5) num objects
    //#output(com.dmdirc.ui.WindowManager__static_init): selectionListener.__Tag
    //#output(com.dmdirc.ui.WindowManager__static_init): rootWindows
    //#output(com.dmdirc.ui.WindowManager__static_init): selListeners
    //#output(com.dmdirc.ui.WindowManager__static_init): selectionListener
    //#new obj(com.dmdirc.ui.WindowManager__static_init): new ArrayList(WindowManager__static_init#1)
    //#new obj(com.dmdirc.ui.WindowManager__static_init): new ArrayList(WindowManager__static_init#3)
    //#new obj(com.dmdirc.ui.WindowManager__static_init): new ArrayList(WindowManager__static_init#4)
    //#new obj(com.dmdirc.ui.WindowManager__static_init): new MapList(WindowManager__static_init#2)
    //#new obj(com.dmdirc.ui.WindowManager__static_init): new WindowManager$WMSelectionListener(WindowManager__static_init#5)
    //#post(com.dmdirc.ui.WindowManager__static_init): __Descendant_Table[com/dmdirc/ui/WindowManager] == &__Dispatch_Table
    //#post(com.dmdirc.ui.WindowManager__static_init): childWindows == &new MapList(WindowManager__static_init#2)
    //#post(com.dmdirc.ui.WindowManager__static_init): frameManagers == &new ArrayList(WindowManager__static_init#3)
    //#post(com.dmdirc.ui.WindowManager__static_init): rootWindows == &new ArrayList(WindowManager__static_init#1)
    //#post(com.dmdirc.ui.WindowManager__static_init): selListeners == &new ArrayList(WindowManager__static_init#4)
    //#post(com.dmdirc.ui.WindowManager__static_init): selectionListener == &new WindowManager$WMSelectionListener(WindowManager__static_init#5)
    //#post(com.dmdirc.ui.WindowManager__static_init): new ArrayList(WindowManager__static_init#1) num objects == 1
    //#post(com.dmdirc.ui.WindowManager__static_init): new ArrayList(WindowManager__static_init#3) num objects == 1
    //#post(com.dmdirc.ui.WindowManager__static_init): new ArrayList(WindowManager__static_init#4) num objects == 1
    //#post(com.dmdirc.ui.WindowManager__static_init): new MapList(WindowManager__static_init#2) num objects == 1
    //#post(com.dmdirc.ui.WindowManager__static_init): new WindowManager$WMSelectionListener(WindowManager__static_init#5) num objects == 1
    //#post(com.dmdirc.ui.WindowManager__static_init): selectionListener.__Tag == com/dmdirc/ui/WindowManager$WMSelectionListener
            = new ArrayList<Window>();

    /** A map of parent windows to their children. */
    private final static MapList<Window, Window> childWindows
    //#WindowManager.java:51: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.util.MapList()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: com.dmdirc.ui.WindowManager__static_init
    //#    unanalyzed callee: void com.dmdirc.util.MapList()
            = new MapList<Window, Window>();

    /** A list of frame managers. */
    private final static List<FrameManager> frameManagers
            = new ArrayList<FrameManager>();
    
    /** A list of selection listeners. */
    private final static List<SelectionListener> selListeners
            = new ArrayList<SelectionListener>();
    
    /** Our selection listener proxy. */
    private static final SelectionListener selectionListener
    //#WindowManager.java:63: end of method: com.dmdirc.ui.WindowManager.com.dmdirc.ui.WindowManager__static_init
            = new WMSelectionListener();

    /**
     * Creates a new instance of WindowManager.
     */
    private WindowManager() {
    //#WindowManager.java:69: method: void com.dmdirc.ui.WindowManager.com.dmdirc.ui.WindowManager()
        // Shouldn't be instansiated
    }
    //#WindowManager.java:71: end of method: void com.dmdirc.ui.WindowManager.com.dmdirc.ui.WindowManager()

    /**
     * Registers a FrameManager with the WindowManager.
     *
     * @param frameManager The frame manager to be registered
     */
    @Precondition({
        "The specified FrameManager is not null",
        "The specified FrameManager has not already been added"
    })
    public static void addFrameManager(final FrameManager frameManager) {
        Logger.assertTrue(frameManager != null);
    //#WindowManager.java:83: method: void com.dmdirc.ui.WindowManager.addFrameManager(FrameManager)
    //#WindowManager.java:83: ?precondition failure
    //#    com/dmdirc/logger/Logger.assertTrue: value == 1
    //#    severity: LOW
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void addFrameManager(FrameManager)
    //#    basic block: bb_4
    //#    assertion: __Temp_Initially_1 == 1
    //#    callee: void com/dmdirc/logger/Logger.assertTrue(bool)
    //#    callee assertion: value == 1
    //#    callee file: Logger.java
    //#    callee precondition index: [1]
    //#    callee srcpos: 92
    //#    VN: __Temp_Initially_1
    //#    Expected: {1}
    //#    Bad: {0}
    //#    Attribs:  Int  Exp in +/-1000  Exp singleton  Bad singleton  Bad overlaps +/-1000  Bad < Exp
    //#input(void addFrameManager(FrameManager)): frameManager
    //#input(void addFrameManager(FrameManager)): frameManagers
        Logger.assertTrue(!frameManagers.contains(frameManager));
    //#WindowManager.java:84: ?precondition failure
    //#    com/dmdirc/logger/Logger.assertTrue: value == 1
    //#    severity: LOW
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void addFrameManager(FrameManager)
    //#    basic block: bb_7
    //#    assertion: __Temp_Initially_1 == 1
    //#    callee: void com/dmdirc/logger/Logger.assertTrue(bool)
    //#    callee assertion: value == 1
    //#    callee file: Logger.java
    //#    callee precondition index: [1]
    //#    callee srcpos: 92
    //#    VN: __Temp_Initially_1
    //#    Expected: {1}
    //#    Bad: {0}
    //#    Attribs:  Int  Exp in +/-1000  Exp singleton  Bad singleton  Bad overlaps +/-1000  Bad < Exp

        frameManagers.add(frameManager);
    }
    //#WindowManager.java:87: end of method: void com.dmdirc.ui.WindowManager.addFrameManager(FrameManager)

    /**
     * Unregisters a FrameManager with the WindowManager.
     *
     * @param frameManager The frame manager to be removed
     */
    @Precondition({
        "The specified FrameManager is not null",
        "The specified FrameManager has already been added and not removed"
    })
    public static void removeFrameManager(final FrameManager frameManager) {
        Logger.assertTrue(frameManager != null);
    //#WindowManager.java:99: method: void com.dmdirc.ui.WindowManager.removeFrameManager(FrameManager)
    //#WindowManager.java:99: ?precondition failure
    //#    com/dmdirc/logger/Logger.assertTrue: value == 1
    //#    severity: LOW
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void removeFrameManager(FrameManager)
    //#    basic block: bb_4
    //#    assertion: __Temp_Initially_1 == 1
    //#    callee: void com/dmdirc/logger/Logger.assertTrue(bool)
    //#    callee assertion: value == 1
    //#    callee file: Logger.java
    //#    callee precondition index: [1]
    //#    callee srcpos: 92
    //#    VN: __Temp_Initially_1
    //#    Expected: {1}
    //#    Bad: {0}
    //#    Attribs:  Int  Exp in +/-1000  Exp singleton  Bad singleton  Bad overlaps +/-1000  Bad < Exp
    //#input(void removeFrameManager(FrameManager)): frameManager
    //#input(void removeFrameManager(FrameManager)): frameManagers
    //#presumption(void removeFrameManager(FrameManager)): java.util.List:contains(...)@100 == 1
        Logger.assertTrue(frameManagers.contains(frameManager));

        frameManagers.remove(frameManager);
    }
    //#WindowManager.java:103: end of method: void com.dmdirc.ui.WindowManager.removeFrameManager(FrameManager)
    
    /**
     * Registers the specified SelectionListener with the WindowManager.
     * 
     * @param listener The listener to be added
     */
    public static void addSelectionListener(final SelectionListener listener) {
        selListeners.add(listener);
    //#WindowManager.java:111: method: void com.dmdirc.ui.WindowManager.addSelectionListener(SelectionListener)
    //#input(void addSelectionListener(SelectionListener)): listener
    //#input(void addSelectionListener(SelectionListener)): selListeners
    }
    //#WindowManager.java:112: end of method: void com.dmdirc.ui.WindowManager.addSelectionListener(SelectionListener)
    
    /**
     * Unregisters the specified SelectionListener with the WindowManager.
     * 
     * @param listener The listener to be removed
     */
    public static void removeSelectionListener(final SelectionListener listener) {
        selListeners.remove(listener);
    //#WindowManager.java:120: method: void com.dmdirc.ui.WindowManager.removeSelectionListener(SelectionListener)
    //#input(void removeSelectionListener(SelectionListener)): listener
    //#input(void removeSelectionListener(SelectionListener)): selListeners
    }
    //#WindowManager.java:121: end of method: void com.dmdirc.ui.WindowManager.removeSelectionListener(SelectionListener)

    /**
     * Adds a new root window to the Window Manager.
     *
     * @param window The window to be added
     */
    @Precondition({
        "The specified Window is not null",
        "The specified Window has not already been added"
    })
    public static void addWindow(final Window window) {
        Logger.assertTrue(window != null);
    //#WindowManager.java:133: method: void com.dmdirc.ui.WindowManager.addWindow(Window)
    //#input(void addWindow(Window)): childWindows
    //#input(void addWindow(Window)): frameManagers
    //#input(void addWindow(Window)): rootWindows
    //#input(void addWindow(Window)): selectionListener
    //#input(void addWindow(Window)): window
    //#pre[1] (void addWindow(Window)): window != null
    //#presumption(void addWindow(Window)): com.dmdirc.ui.interfaces.Window:getContainer(...)@139 != null
    //#unanalyzed(void addWindow(Window)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(void addWindow(Window)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void addWindow(Window)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void addWindow(Window)): Effects-of-calling:com.dmdirc.ui.interfaces.Window:getContainer
    //#unanalyzed(void addWindow(Window)): Effects-of-calling:com.dmdirc.ui.interfaces.FrameManager:addWindow
        Logger.assertTrue(!rootWindows.contains(window));
    //#WindowManager.java:134: ?precondition failure
    //#    com/dmdirc/logger/Logger.assertTrue: value == 1
    //#    severity: LOW
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void addWindow(Window)
    //#    basic block: bb_7
    //#    assertion: __Temp_Initially_1 == 1
    //#    callee: void com/dmdirc/logger/Logger.assertTrue(bool)
    //#    callee assertion: value == 1
    //#    callee file: Logger.java
    //#    callee precondition index: [1]
    //#    callee srcpos: 92
    //#    VN: __Temp_Initially_1
    //#    Expected: {1}
    //#    Bad: {0}
    //#    Attribs:  Int  Exp in +/-1000  Exp singleton  Bad singleton  Bad overlaps +/-1000  Bad < Exp

        rootWindows.add(window);
        childWindows.add(window);
    //#WindowManager.java:137: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.util.MapList:add(Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void addWindow(Window)
    //#    unanalyzed callee: void com.dmdirc.util.MapList:add(Object)
        
        window.getContainer().addSelectionListener(selectionListener);
    //#WindowManager.java:139: Warning: method not available - call not analyzed
    //#    call on FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void addWindow(Window)
    //#    unanalyzed callee: FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#WindowManager.java:139: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.FrameContainer:addSelectionListener(SelectionListener)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void addWindow(Window)
    //#    unanalyzed callee: void com.dmdirc.FrameContainer:addSelectionListener(SelectionListener)

        fireAddWindow(window);
    }
    //#WindowManager.java:142: end of method: void com.dmdirc.ui.WindowManager.addWindow(Window)

    /**
     * Adds a new child window to the Window Manager.
     *
     * @param parent The parent window
     * @param child The child window to be added
     */
    @Precondition({
        "The specified Windows are not null",
        "The parent Window has already been added",
        "The child Window has not already been added"
    })
    public static void addWindow(final Window parent, final Window child) {
        Logger.assertTrue(parent != null);
    //#WindowManager.java:156: method: void com.dmdirc.ui.WindowManager.addWindow(Window, Window)
    //#input(void addWindow(Window, Window)): child
    //#input(void addWindow(Window, Window)): childWindows
    //#input(void addWindow(Window, Window)): frameManagers
    //#input(void addWindow(Window, Window)): parent
    //#input(void addWindow(Window, Window)): selectionListener
    //#pre[1] (void addWindow(Window, Window)): child != null
    //#pre[2] (void addWindow(Window, Window)): (soft) parent != null
    //#presumption(void addWindow(Window, Window)): com.dmdirc.ui.interfaces.Window:getContainer(...)@164 != null
    //#presumption(void addWindow(Window, Window)): com.dmdirc.util.MapList:containsKey(...)@158 == 1
    //#unanalyzed(void addWindow(Window, Window)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(void addWindow(Window, Window)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void addWindow(Window, Window)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void addWindow(Window, Window)): Effects-of-calling:com.dmdirc.ui.interfaces.Window:getContainer
    //#unanalyzed(void addWindow(Window, Window)): Effects-of-calling:com.dmdirc.ui.interfaces.FrameManager:addWindow
        Logger.assertTrue(child != null);
        Logger.assertTrue(childWindows.containsKey(parent));
    //#WindowManager.java:158: Warning: method not available - call not analyzed
    //#    call on bool com.dmdirc.util.MapList:containsKey(Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void addWindow(Window, Window)
    //#    unanalyzed callee: bool com.dmdirc.util.MapList:containsKey(Object)
        Logger.assertTrue(!childWindows.containsKey(child));
    //#WindowManager.java:159: Warning: method not available - call not analyzed
    //#    call on bool com.dmdirc.util.MapList:containsKey(Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void addWindow(Window, Window)
    //#    unanalyzed callee: bool com.dmdirc.util.MapList:containsKey(Object)
    //#WindowManager.java:159: ?precondition failure
    //#    com/dmdirc/logger/Logger.assertTrue: value == 1
    //#    severity: LOW
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void addWindow(Window, Window)
    //#    basic block: bb_10
    //#    assertion: __Temp_Initially_1 == 1
    //#    callee: void com/dmdirc/logger/Logger.assertTrue(bool)
    //#    callee assertion: value == 1
    //#    callee file: Logger.java
    //#    callee precondition index: [1]
    //#    callee srcpos: 92
    //#    VN: __Temp_Initially_1
    //#    Expected: {1}
    //#    Bad: {0}
    //#    Attribs:  Int  Exp in +/-1000  Exp singleton  Bad singleton  Bad overlaps +/-1000  Bad < Exp

        childWindows.add(parent, child);
    //#WindowManager.java:161: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.util.MapList:add(Object, Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void addWindow(Window, Window)
    //#    unanalyzed callee: void com.dmdirc.util.MapList:add(Object, Object)
        childWindows.add(child);
    //#WindowManager.java:162: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.util.MapList:add(Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void addWindow(Window, Window)
    //#    unanalyzed callee: void com.dmdirc.util.MapList:add(Object)
        
        child.getContainer().addSelectionListener(selectionListener);
    //#WindowManager.java:164: Warning: method not available - call not analyzed
    //#    call on FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void addWindow(Window, Window)
    //#    unanalyzed callee: FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#WindowManager.java:164: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.FrameContainer:addSelectionListener(SelectionListener)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void addWindow(Window, Window)
    //#    unanalyzed callee: void com.dmdirc.FrameContainer:addSelectionListener(SelectionListener)

        fireAddWindow(parent, child);
    }
    //#WindowManager.java:167: end of method: void com.dmdirc.ui.WindowManager.addWindow(Window, Window)

    /**
     * Removes a window from the Window Manager. If the specified window
     * has child windows, they are recursively removed before the target window.
     * If the window hasn't previously been added, the reques to remove it is
     * ignored.
     *
     * @param window The window to be removed
     */
    @Precondition("The specified Window is not null")
    public static void removeWindow(final Window window) {
        Logger.assertTrue(window != null);
    //#WindowManager.java:179: method: void com.dmdirc.ui.WindowManager.removeWindow(Window)
    //#input(void removeWindow(Window)): "&#09;"._tainted
    //#input(void removeWindow(Window)): "&#10;Which caused: "._tainted
    //#input(void removeWindow(Window)): "-"._tainted
    //#input(void removeWindow(Window)): ".log"._tainted
    //#input(void removeWindow(Window)): ": "._tainted
    //#input(void removeWindow(Window)): "A fatal error has occurred: "._tainted
    //#input(void removeWindow(Window)): "An error has occurred: "._tainted
    //#input(void removeWindow(Window)): "Date:"._tainted
    //#input(void removeWindow(Window)): "Description: "._tainted
    //#input(void removeWindow(Window)): "ID must be a positive integer: "._tainted
    //#input(void removeWindow(Window)): "Invalid window removed"._tainted
    //#input(void removeWindow(Window)): "Level: "._tainted
    //#input(void removeWindow(Window)): "Tried to remove a non-root window that has no known parent.&#10;Window: "._tainted
    //#input(void removeWindow(Window)): "errors"._tainted
    //#input(void removeWindow(Window)): childWindows
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorLevel__static_init.new ErrorLevel(ErrorLevel__static_init#3)._tainted
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorManager__static_init.new Class[](ErrorManager__static_init#2).length
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorManager__static_init.new Class[](ErrorManager__static_init#2)[0..4_294_967_295]
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).errorListeners
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).errors
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).errors.__Lock
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).logReports
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).nextErrorID
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).reportQueue
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).reportThread
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).sendReports
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorReportStatus__static_init.new ErrorReportStatus(ErrorReportStatus__static_init#1).terminal
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorReportStatus__static_init.new ErrorReportStatus(ErrorReportStatus__static_init#5).terminal
    //#input(void removeWindow(Window)): com.dmdirc.logger.ErrorReportStatus__static_init.new ErrorReportStatus(ErrorReportStatus__static_init#6).terminal
    //#input(void removeWindow(Window)): com.dmdirc.ui.FatalErrorDialog$4__static_init.new int[](FatalErrorDialog$4__static_init#1).length
    //#input(void removeWindow(Window)): com.dmdirc.ui.FatalErrorDialog$4__static_init.new int[](FatalErrorDialog$4__static_init#1)[0..4_294_967_295]
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorFixedStatus.INVALID
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorFixedStatus.KNOWN
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorFixedStatus.UNKNOWN
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorFixedStatus.UNREPORTED
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorLevel.FATAL
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorLevel.MEDIUM
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorListener.__Descendant_Table[com/dmdirc/logger/ErrorListener]
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorListener.__Descendant_Table[com/dmdirc/ui/FatalErrorDialog]
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorListener.__Descendant_Table[others]
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorListener.__Dispatch_Table.errorAdded(Lcom/dmdirc/logger/ProgramError;)V
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorListener.__Dispatch_Table.errorStatusChanged(Lcom/dmdirc/logger/ProgramError;)V
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorListener.__Dispatch_Table.isReady()Z
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorManager.BANNED_EXCEPTIONS
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorManager.java.lang.System.err
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorManager.me
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorReportStatus.ERROR
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorReportStatus.NOT_APPLICABLE
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorReportStatus.QUEUED
    //#input(void removeWindow(Window)): com/dmdirc/logger/ErrorReportStatus.WAITING
    //#input(void removeWindow(Window)): com/dmdirc/logger/Logger.manager
    //#input(void removeWindow(Window)): com/dmdirc/logger/ProgramError.__Descendant_Table[com/dmdirc/logger/ProgramError]
    //#input(void removeWindow(Window)): com/dmdirc/logger/ProgramError.__Descendant_Table[others]
    //#input(void removeWindow(Window)): com/dmdirc/logger/ProgramError.errorDir
    //#input(void removeWindow(Window)): com/dmdirc/logger/ProgramError.java.lang.System.err
    //#input(void removeWindow(Window)): com/dmdirc/logger/ProgramError.writingSem
    //#input(void removeWindow(Window)): com/dmdirc/ui/FatalErrorDialog$4.$SwitchMap$com$dmdirc$logger$ErrorReportStatus
    //#input(void removeWindow(Window)): com/dmdirc/ui/FatalErrorDialog.__Dispatch_Table.errorAdded(Lcom/dmdirc/logger/ProgramError;)V
    //#input(void removeWindow(Window)): com/dmdirc/ui/FatalErrorDialog.__Dispatch_Table.errorStatusChanged(Lcom/dmdirc/logger/ProgramError;)V
    //#input(void removeWindow(Window)): com/dmdirc/ui/FatalErrorDialog.__Dispatch_Table.isReady()Z
    //#input(void removeWindow(Window)): frameManagers
    //#input(void removeWindow(Window)): rootWindows
    //#input(void removeWindow(Window)): selectionListener
    //#input(void removeWindow(Window)): window
    //#output(void removeWindow(Window)): com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).reportThread
    //#output(void removeWindow(Window)): com/dmdirc/logger/ProgramError.errorDir
    //#output(void removeWindow(Window)): new ErrorReportingThread(sendError#1) num objects
    //#output(void removeWindow(Window)): new ErrorReportingThread(sendError#1).__Tag
    //#output(void removeWindow(Window)): new ErrorReportingThread(sendError#1).queue
    //#output(void removeWindow(Window)): new File(getErrorFile#1) num objects
    //#new obj(void removeWindow(Window)): new ErrorReportingThread(sendError#1)
    //#new obj(void removeWindow(Window)): new File(getErrorFile#1)
    //#pre[3] (void removeWindow(Window)): (soft) com.dmdirc.logger.ErrorManager__static_init.new Class[](ErrorManager__static_init#2)[0..4_294_967_295] != null
    //#pre[5] (void removeWindow(Window)): (soft) init'ed(com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).logReports)
    //#pre[6] (void removeWindow(Window)): (soft) com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).nextErrorID != null
    //#pre[7] (void removeWindow(Window)): (soft) init'ed(com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).sendReports)
    //#pre[8] (void removeWindow(Window)): (soft) init'ed(com.dmdirc.ui.FatalErrorDialog$4__static_init.new int[](FatalErrorDialog$4__static_init#1)[0..4_294_967_295])
    //#pre[10] (void removeWindow(Window)): (soft) init'ed(com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).reportThread)
    //#pre[11] (void removeWindow(Window)): (soft) init'ed(com/dmdirc/logger/ProgramError.errorDir)
    //#pre[12] (void removeWindow(Window)): (soft) window != null
    //#presumption(void removeWindow(Window)): com.dmdirc.logger.ErrorManager__static_init.new Class[](ErrorManager__static_init#2)[0..4_294_967_295]@193 != null
    //#presumption(void removeWindow(Window)): com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).nextErrorID@193 != null
    //#presumption(void removeWindow(Window)): com.dmdirc.ui.interfaces.Window:getContainer(...)@228 != null
    //#presumption(void removeWindow(Window)): com.dmdirc.util.MapList:get(...)@185 != null
    //#presumption(void removeWindow(Window)): com.dmdirc.util.MapList:get(...)@190 != null
    //#presumption(void removeWindow(Window)): java.util.ArrayList:iterator(...)@186 != null
    //#presumption(void removeWindow(Window)): java.util.Iterator:next(...)@186 != null
    //#post(void removeWindow(Window)): init'ed(com/dmdirc/logger/ProgramError.errorDir)
    //#post(void removeWindow(Window)): init'ed(com.dmdirc.logger.ErrorManager__static_init.new ErrorManager(ErrorManager__static_init#1).reportThread)
    //#post(void removeWindow(Window)): new ErrorReportingThread(sendError#1) num objects <= 1
    //#post(void removeWindow(Window)): init'ed(new ErrorReportingThread(sendError#1).__Tag)
    //#post(void removeWindow(Window)): init'ed(new ErrorReportingThread(sendError#1).queue)
    //#post(void removeWindow(Window)): new File(getErrorFile#1) num objects <= 1
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.List:contains
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:com.dmdirc.ui.interfaces.Window:getContainer
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:com.dmdirc.ui.interfaces.FrameManager:delWindow
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:com.dmdirc.util.MapList:entrySet
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.Set:iterator
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.Map$Entry:getValue
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.Throwable:__curr_excep_obj
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.Map$Entry:getKey
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:getErrorManager
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:addError
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.concurrent.atomic.AtomicLong:getAndIncrement
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.Date
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.StringBuilder
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.StringBuilder:append
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.StringBuilder:toString
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.IllegalArgumentException
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.String:isEmpty
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.Arrays:copyOf
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.Date:clone
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.List:add
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:com.dmdirc.logger.ErrorReportStatus:equals
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:fireErrorStatusChanged
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.Object:notifyAll
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.concurrent.BlockingQueue:add
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.Thread:isAlive
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.Thread
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:com.dmdirc.logger.ErrorReportingThread:setDaemon
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.Thread:start
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.awt.GraphicsEnvironment:isHeadless
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.io.PrintStream:println
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:javax.swing.SwingUtilities:invokeLater
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.concurrent.Semaphore
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.concurrent.Semaphore:acquireUninterruptibly
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.Object:wait
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:com.dmdirc.util.ListenerList:get
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:isReady
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:errorAdded
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:com.dmdirc.logger.ErrorFixedStatus:equals
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.String:startsWith
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.io.File:exists
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:com.dmdirc.Main:getConfigDir
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.io.File
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.io.File:mkdirs
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.Date:getTime
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.io.File:renameTo
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.io.File:createNewFile
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.io.FileOutputStream
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.concurrent.Semaphore:release
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.io.IOException:printStackTrace
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.io.OutputStream
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.io.PrintWriter
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.io.PrintWriter:println
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.io.PrintWriter:close
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.Throwable:getStackTrace
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.Throwable:toString
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.StackTraceElement:toString
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.Throwable:getCause
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:getTrace
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.Object:getClass
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.Object:equals
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:com.dmdirc.logger.ErrorReportStatus:ordinal
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:javax.swing.JButton:setText
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:javax.swing.JButton:setEnabled
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:equals
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:getReportStatus
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:errorStatusChanged
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.lang.String:equals
    //#unanalyzed(void removeWindow(Window)): Effects-of-calling:java.util.Arrays:equals
    //#test_vector(void removeWindow(Window)): com.dmdirc.util.MapList:containsKey(...)@181: {1}, {0}
    //#test_vector(void removeWindow(Window)): com.dmdirc.util.MapList:get(...)@185: Addr_Set{null}, Inverse{null}
    //#test_vector(void removeWindow(Window)): java.util.Iterator:hasNext(...)@186: {0}, {1}
    //#test_vector(void removeWindow(Window)): java.util.List:contains(...)@205: {0}, {1}
    //#test_vector(void removeWindow(Window)): java.util.List:isEmpty(...)@185: {1}, {0}
    //#test_vector(void removeWindow(Window)): java.util.List:isEmpty(...)@190: {1}, {0}
        
        if (!childWindows.containsKey(window)) {
    //#WindowManager.java:181: Warning: method not available - call not analyzed
    //#    call on bool com.dmdirc.util.MapList:containsKey(Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void removeWindow(Window)
    //#    unanalyzed callee: bool com.dmdirc.util.MapList:containsKey(Object)
            return;
        }

        if (childWindows.get(window) != null && !childWindows.get(window).isEmpty()) {
    //#WindowManager.java:185: Warning: method not available - call not analyzed
    //#    call on List com.dmdirc.util.MapList:get(Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void removeWindow(Window)
    //#    unanalyzed callee: List com.dmdirc.util.MapList:get(Object)
            for (Window child : new ArrayList<Window>(childWindows.get(window))) {
    //#WindowManager.java:186: Warning: method not available - call not analyzed
    //#    call on List com.dmdirc.util.MapList:get(Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void removeWindow(Window)
    //#    unanalyzed callee: List com.dmdirc.util.MapList:get(Object)
                child.close();
    //#WindowManager.java:187: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.ui.interfaces.Window:close()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void removeWindow(Window)
    //#    unanalyzed callee: void com.dmdirc.ui.interfaces.Window:close()
            }

            while (!childWindows.get(window).isEmpty()) {
    //#WindowManager.java:190: Warning: method not available - call not analyzed
    //#    call on List com.dmdirc.util.MapList:get(Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void removeWindow(Window)
    //#    unanalyzed callee: List com.dmdirc.util.MapList:get(Object)
                try {
                    synchronized (childWindows) {
                        childWindows.wait();
                    }
                } catch (InterruptedException ex) {
                    // Ignore it
                }
            }
        }

        synchronized (childWindows) {
            childWindows.remove(window);
    //#WindowManager.java:202: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.util.MapList:remove(Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void removeWindow(Window)
    //#    unanalyzed callee: void com.dmdirc.util.MapList:remove(Object)
        }

        if (rootWindows.contains(window)) {
            rootWindows.remove(window);

            fireDeleteWindow(window);
        } else {
            final Window parent = getParent(window);

            if (parent == null) {
                Logger.appError(ErrorLevel.MEDIUM, "Invalid window removed",
    //#WindowManager.java:213: Warning: method not available - call not analyzed
    //#    call on String com.dmdirc.ui.interfaces.Window:getTitle()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void removeWindow(Window)
    //#    unanalyzed callee: String com.dmdirc.ui.interfaces.Window:getTitle()
                        new IllegalArgumentException("Tried to remove a" +
                        " non-root window that has no known parent.\nWindow:" +
                        " " + window.getTitle()));
                return;
            } else {
                synchronized (childWindows) {
                    childWindows.remove(parent, window);
    //#WindowManager.java:220: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.util.MapList:remove(Object, Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void removeWindow(Window)
    //#    unanalyzed callee: void com.dmdirc.util.MapList:remove(Object, Object)
                    childWindows.notifyAll();
                }

                fireDeleteWindow(parent, window);
            }
        }
        
        window.getContainer().removeSelectionListener(selectionListener);
    //#WindowManager.java:228: Warning: method not available - call not analyzed
    //#    call on FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void removeWindow(Window)
    //#    unanalyzed callee: FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#WindowManager.java:228: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.FrameContainer:removeSelectionListener(SelectionListener)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void removeWindow(Window)
    //#    unanalyzed callee: void com.dmdirc.FrameContainer:removeSelectionListener(SelectionListener)
    }
    //#WindowManager.java:229: end of method: void com.dmdirc.ui.WindowManager.removeWindow(Window)

    /**
     * Finds and returns a global custom window with the specified name.
     * If a custom window with the specified name isn't found, null is returned.
     * 
     * @param name The name of the custom window to search for
     * @return The specified custom window, or null
     */
    @Precondition("The specified window name is not null")
    public static Window findCustomWindow(final String name) {
        Logger.assertTrue(name != null);
    //#WindowManager.java:240: method: Window com.dmdirc.ui.WindowManager.findCustomWindow(String)
    //#WindowManager.java:240: ?precondition failure
    //#    com/dmdirc/logger/Logger.assertTrue: value == 1
    //#    severity: LOW
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: Window findCustomWindow(String)
    //#    basic block: bb_4
    //#    assertion: __Temp_Initially_1 == 1
    //#    callee: void com/dmdirc/logger/Logger.assertTrue(bool)
    //#    callee assertion: value == 1
    //#    callee file: Logger.java
    //#    callee precondition index: [1]
    //#    callee srcpos: 92
    //#    VN: __Temp_Initially_1
    //#    Expected: {1}
    //#    Bad: {0}
    //#    Attribs:  Int  Exp in +/-1000  Exp singleton  Bad singleton  Bad overlaps +/-1000  Bad < Exp
    //#input(Window findCustomWindow(String)): name
    //#input(Window findCustomWindow(String)): rootWindows
    //#output(Window findCustomWindow(String)): return_value
    //#post(Window findCustomWindow(String)): init'ed(return_value)
    //#unanalyzed(Window findCustomWindow(String)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(Window findCustomWindow(String)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(Window findCustomWindow(String)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(Window findCustomWindow(String)): Effects-of-calling:com.dmdirc.ui.interfaces.Window:getContainer
    //#unanalyzed(Window findCustomWindow(String)): Effects-of-calling:com.dmdirc.CustomWindow:instanceof
    //#unanalyzed(Window findCustomWindow(String)): Effects-of-calling:com.dmdirc.CustomWindow:getName
    //#unanalyzed(Window findCustomWindow(String)): Effects-of-calling:java.lang.String:equals

        return findCustomWindow(rootWindows, name);
    //#WindowManager.java:242: end of method: Window com.dmdirc.ui.WindowManager.findCustomWindow(String)
    }

    /**
     * Finds and returns a non-global custom window with the specified name.
     * If a custom window with the specified name isn't found, null is returned.
     * 
     * @param parent The parent whose children should be searched
     * @param name The name of the custom window to search for
     * @return The specified custom window, or null
     */
    @Precondition({
        "The specified window name is not null",
        "The specified parent window is not null",
        "The specified parent window has been added to the Window Manager"
    })
    public static Window findCustomWindow(final Window parent, final String name) {
        Logger.assertTrue(parent != null);
    //#WindowManager.java:259: method: Window com.dmdirc.ui.WindowManager.findCustomWindow(Window, String)
    //#WindowManager.java:259: ?precondition failure
    //#    com/dmdirc/logger/Logger.assertTrue: value == 1
    //#    severity: LOW
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: Window findCustomWindow(Window, String)
    //#    basic block: bb_4
    //#    assertion: __Temp_Initially_1 == 1
    //#    callee: void com/dmdirc/logger/Logger.assertTrue(bool)
    //#    callee assertion: value == 1
    //#    callee file: Logger.java
    //#    callee precondition index: [1]
    //#    callee srcpos: 92
    //#    VN: __Temp_Initially_1
    //#    Expected: {1}
    //#    Bad: {0}
    //#    Attribs:  Int  Exp in +/-1000  Exp singleton  Bad singleton  Bad overlaps +/-1000  Bad < Exp
    //#input(Window findCustomWindow(Window, String)): childWindows
    //#input(Window findCustomWindow(Window, String)): name
    //#input(Window findCustomWindow(Window, String)): parent
    //#output(Window findCustomWindow(Window, String)): return_value
    //#presumption(Window findCustomWindow(Window, String)): com.dmdirc.util.MapList:containsKey(...)@261 == 1
    //#presumption(Window findCustomWindow(Window, String)): com.dmdirc.util.MapList:get(...)@263 != null
    //#post(Window findCustomWindow(Window, String)): init'ed(return_value)
    //#unanalyzed(Window findCustomWindow(Window, String)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(Window findCustomWindow(Window, String)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(Window findCustomWindow(Window, String)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(Window findCustomWindow(Window, String)): Effects-of-calling:com.dmdirc.ui.interfaces.Window:getContainer
    //#unanalyzed(Window findCustomWindow(Window, String)): Effects-of-calling:com.dmdirc.CustomWindow:instanceof
    //#unanalyzed(Window findCustomWindow(Window, String)): Effects-of-calling:com.dmdirc.CustomWindow:getName
    //#unanalyzed(Window findCustomWindow(Window, String)): Effects-of-calling:java.lang.String:equals
        Logger.assertTrue(name != null);
    //#WindowManager.java:260: ?precondition failure
    //#    com/dmdirc/logger/Logger.assertTrue: value == 1
    //#    severity: LOW
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: Window findCustomWindow(Window, String)
    //#    basic block: bb_7
    //#    assertion: __Temp_Initially_1 == 1
    //#    callee: void com/dmdirc/logger/Logger.assertTrue(bool)
    //#    callee assertion: value == 1
    //#    callee file: Logger.java
    //#    callee precondition index: [1]
    //#    callee srcpos: 92
    //#    VN: __Temp_Initially_1
    //#    Expected: {1}
    //#    Bad: {0}
    //#    Attribs:  Int  Exp in +/-1000  Exp singleton  Bad singleton  Bad overlaps +/-1000  Bad < Exp
        Logger.assertTrue(childWindows.containsKey(parent));
    //#WindowManager.java:261: Warning: method not available - call not analyzed
    //#    call on bool com.dmdirc.util.MapList:containsKey(Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: Window findCustomWindow(Window, String)
    //#    unanalyzed callee: bool com.dmdirc.util.MapList:containsKey(Object)

        return findCustomWindow(childWindows.get(parent), name);
    //#WindowManager.java:263: Warning: method not available - call not analyzed
    //#    call on List com.dmdirc.util.MapList:get(Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: Window findCustomWindow(Window, String)
    //#    unanalyzed callee: List com.dmdirc.util.MapList:get(Object)
    //#WindowManager.java:263: end of method: Window com.dmdirc.ui.WindowManager.findCustomWindow(Window, String)
    }

    /**
     * Finds a custom window with the specified name among the specified list
     * of windows. If the custom window is not found, returns null.
     * 
     * @param windows The list of windows to search
     * @param name The name of the custom window to search for
     * @return The custom window if found, or null otherwise
     */
    private static Window findCustomWindow(final List<Window> windows, final String name) {
        for (Window window : windows) {
    //#WindowManager.java:275: method: Window com.dmdirc.ui.WindowManager.findCustomWindow(List, String)
    //#input(Window findCustomWindow(List, String)): name
    //#input(Window findCustomWindow(List, String)): windows
    //#output(Window findCustomWindow(List, String)): return_value
    //#pre[2] (Window findCustomWindow(List, String)): windows != null
    //#presumption(Window findCustomWindow(List, String)): com.dmdirc.CustomWindow:getName(...)@276 != null
    //#presumption(Window findCustomWindow(List, String)): com.dmdirc.ui.interfaces.Window:getContainer(...)@276 != null
    //#presumption(Window findCustomWindow(List, String)): java.util.Iterator:next(...)@275 != null
    //#post(Window findCustomWindow(List, String)): init'ed(return_value)
    //#test_vector(Window findCustomWindow(List, String)): java.lang.String:equals(...)@276: {0}, {1}
    //#test_vector(Window findCustomWindow(List, String)): java.util.Iterator:hasNext(...)@275: {0}, {1}
            if (window.getContainer() instanceof CustomWindow
    //#WindowManager.java:276: Warning: method not available - call not analyzed
    //#    call on FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: Window findCustomWindow(List, String)
    //#    unanalyzed callee: FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#WindowManager.java:276: Warning: method not available - call not analyzed
    //#    call on String com.dmdirc.CustomWindow:getName()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: Window findCustomWindow(List, String)
    //#    unanalyzed callee: String com.dmdirc.CustomWindow:getName()
                    && ((CustomWindow) window.getContainer()).getName().equals(name)) {
                return window;
            }
        }

        return null;
    //#WindowManager.java:282: end of method: Window com.dmdirc.ui.WindowManager.findCustomWindow(List, String)
    }

    /**
     * Retrieves the parent window of the specified window. If the window
     * has no parent (i.e., it is a root window or it has not been added),
     * returns null.
     * 
     * @param window The window whose parent is being sought
     * @return The parent of the specified window, or null if not found
     */
    public static Window getParent(final Window window) {
        synchronized (childWindows) {
    //#WindowManager.java:294: method: Window com.dmdirc.ui.WindowManager.getParent(Window)
    //#input(Window getParent(Window)): childWindows
    //#input(Window getParent(Window)): childWindows.__Lock
    //#input(Window getParent(Window)): window
    //#output(Window getParent(Window)): return_value
    //#presumption(Window getParent(Window)): com.dmdirc.util.MapList:entrySet(...)@295 != null
    //#presumption(Window getParent(Window)): java.util.Iterator:next(...)@295 != null
    //#presumption(Window getParent(Window)): java.util.Map_Entry:getValue(...)@296 != null
    //#post(Window getParent(Window)): init'ed(return_value)
    //#test_vector(Window getParent(Window)): java.util.Iterator:hasNext(...)@295: {1}, {0}
    //#test_vector(Window getParent(Window)): java.util.List:contains(...)@296: {0}, {1}
            for (Entry<Window, List<Window>> entry : childWindows.entrySet()) {
    //#WindowManager.java:295: Warning: method not available - call not analyzed
    //#    call on Set com.dmdirc.util.MapList:entrySet()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: Window getParent(Window)
    //#    unanalyzed callee: Set com.dmdirc.util.MapList:entrySet()
                if (entry.getValue().contains(window)) {
                    return entry.getKey();
                }
            }
        }

        return null;
    //#WindowManager.java:302: end of method: Window com.dmdirc.ui.WindowManager.getParent(Window)
    }
    
    /**
     * Retrieves all known root (parent-less) windows.
     * 
     * @since 0.6
     * @return An array of all known root windows.
     */
    public static Window[] getRootWindows() {
        return rootWindows.toArray(new Window[rootWindows.size()]);
    //#WindowManager.java:312: method: Window[] com.dmdirc.ui.WindowManager.getRootWindows()
    //#input(Window[] getRootWindows()): rootWindows
    //#output(Window[] getRootWindows()): return_value
    //#presumption(Window[] getRootWindows()): java.util.List:size(...)@312 >= 0
    //#post(Window[] getRootWindows()): init'ed(return_value)
    //#WindowManager.java:312: end of method: Window[] com.dmdirc.ui.WindowManager.getRootWindows()
    }
    
    /**
     * Retrieves all children of the specified window.
     * 
     * @since 0.6
     * @param window The window whose children are being requested
     * @return An array of all known child windows.
     */
    public static Window[] getChildren(final Window window) {
        final List<Window> children = childWindows.get(window);
    //#WindowManager.java:323: method: Window[] com.dmdirc.ui.WindowManager.getChildren(Window)
    //#WindowManager.java:323: Warning: method not available - call not analyzed
    //#    call on List com.dmdirc.util.MapList:get(Object)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: Window[] getChildren(Window)
    //#    unanalyzed callee: List com.dmdirc.util.MapList:get(Object)
    //#input(Window[] getChildren(Window)): childWindows
    //#input(Window[] getChildren(Window)): window
    //#output(Window[] getChildren(Window)): return_value
    //#presumption(Window[] getChildren(Window)): com.dmdirc.util.MapList:get(...)@323 != null
    //#presumption(Window[] getChildren(Window)): java.util.List:size(...)@324 >= 0
    //#post(Window[] getChildren(Window)): init'ed(return_value)
        return children.toArray(new Window[children.size()]);
    //#WindowManager.java:324: end of method: Window[] com.dmdirc.ui.WindowManager.getChildren(Window)
    }
    
    /**
     * Fires the addWindow(Window) callback.
     * 
     * @param window The window that was added
     */
    private static void fireAddWindow(final Window window) {
        for (FrameManager manager : frameManagers) {
    //#WindowManager.java:333: method: void com.dmdirc.ui.WindowManager.fireAddWindow(Window)
    //#input(void fireAddWindow(Window)): frameManagers
    //#input(void fireAddWindow(Window)): window
    //#pre[1] (void fireAddWindow(Window)): (soft) window != null
    //#presumption(void fireAddWindow(Window)): java.util.Iterator:next(...)@333 != null
    //#test_vector(void fireAddWindow(Window)): java.util.Iterator:hasNext(...)@333: {0}, {1}
            manager.addWindow(window.getContainer());
    //#WindowManager.java:334: Warning: method not available - call not analyzed
    //#    call on FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void fireAddWindow(Window)
    //#    unanalyzed callee: FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#WindowManager.java:334: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.ui.interfaces.FrameManager:addWindow(FrameContainer)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void fireAddWindow(Window)
    //#    unanalyzed callee: void com.dmdirc.ui.interfaces.FrameManager:addWindow(FrameContainer)
        }
    }
    //#WindowManager.java:336: end of method: void com.dmdirc.ui.WindowManager.fireAddWindow(Window)

    /**
     * Fires the addWindow(Window, Window) callback.
     * 
     * @param parent The parent window
     * @param child The new child window that was added
     */
    private static void fireAddWindow(final Window parent, final Window child) {
        for (FrameManager manager : frameManagers) {
    //#WindowManager.java:345: method: void com.dmdirc.ui.WindowManager.fireAddWindow(Window, Window)
    //#input(void fireAddWindow(Window, Window)): child
    //#input(void fireAddWindow(Window, Window)): frameManagers
    //#input(void fireAddWindow(Window, Window)): parent
    //#pre[1] (void fireAddWindow(Window, Window)): (soft) child != null
    //#pre[2] (void fireAddWindow(Window, Window)): (soft) parent != null
    //#presumption(void fireAddWindow(Window, Window)): java.util.Iterator:next(...)@345 != null
    //#test_vector(void fireAddWindow(Window, Window)): java.util.Iterator:hasNext(...)@345: {0}, {1}
            manager.addWindow(parent.getContainer(), child.getContainer());
    //#WindowManager.java:346: Warning: method not available - call not analyzed
    //#    call on FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void fireAddWindow(Window, Window)
    //#    unanalyzed callee: FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#WindowManager.java:346: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.ui.interfaces.FrameManager:addWindow(FrameContainer, FrameContainer)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void fireAddWindow(Window, Window)
    //#    unanalyzed callee: void com.dmdirc.ui.interfaces.FrameManager:addWindow(FrameContainer, FrameContainer)
        }
    }
    //#WindowManager.java:348: end of method: void com.dmdirc.ui.WindowManager.fireAddWindow(Window, Window)

    /**
     * Fires the delWindow(Window) callback.
     * 
     * @param window The window that was removed
     */
    private static void fireDeleteWindow(final Window window) {
        for (FrameManager manager : frameManagers) {
    //#WindowManager.java:356: method: void com.dmdirc.ui.WindowManager.fireDeleteWindow(Window)
    //#input(void fireDeleteWindow(Window)): frameManagers
    //#input(void fireDeleteWindow(Window)): window
    //#pre[1] (void fireDeleteWindow(Window)): (soft) window != null
    //#presumption(void fireDeleteWindow(Window)): java.util.Iterator:next(...)@356 != null
    //#test_vector(void fireDeleteWindow(Window)): java.util.Iterator:hasNext(...)@356: {0}, {1}
            manager.delWindow(window.getContainer());
    //#WindowManager.java:357: Warning: method not available - call not analyzed
    //#    call on FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void fireDeleteWindow(Window)
    //#    unanalyzed callee: FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#WindowManager.java:357: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.ui.interfaces.FrameManager:delWindow(FrameContainer)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void fireDeleteWindow(Window)
    //#    unanalyzed callee: void com.dmdirc.ui.interfaces.FrameManager:delWindow(FrameContainer)
        }
    }
    //#WindowManager.java:359: end of method: void com.dmdirc.ui.WindowManager.fireDeleteWindow(Window)

    /**
     * Fires the delWindow(Window, Window) callback.
     * 
     * @param parent The parent window
     * @param child The child window that was removed
     */
    private static void fireDeleteWindow(final Window parent, final Window child) {
        for (FrameManager manager : frameManagers) {
    //#WindowManager.java:368: method: void com.dmdirc.ui.WindowManager.fireDeleteWindow(Window, Window)
    //#input(void fireDeleteWindow(Window, Window)): child
    //#input(void fireDeleteWindow(Window, Window)): frameManagers
    //#input(void fireDeleteWindow(Window, Window)): parent
    //#pre[1] (void fireDeleteWindow(Window, Window)): (soft) child != null
    //#pre[2] (void fireDeleteWindow(Window, Window)): (soft) parent != null
    //#presumption(void fireDeleteWindow(Window, Window)): java.util.Iterator:next(...)@368 != null
    //#test_vector(void fireDeleteWindow(Window, Window)): java.util.Iterator:hasNext(...)@368: {0}, {1}
            manager.delWindow(parent.getContainer(), child.getContainer());
    //#WindowManager.java:369: Warning: method not available - call not analyzed
    //#    call on FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void fireDeleteWindow(Window, Window)
    //#    unanalyzed callee: FrameContainer com.dmdirc.ui.interfaces.Window:getContainer()
    //#WindowManager.java:369: Warning: method not available - call not analyzed
    //#    call on void com.dmdirc.ui.interfaces.FrameManager:delWindow(FrameContainer, FrameContainer)
    //#    severity: INFORMATIONAL
    //#    class: com.dmdirc.ui.WindowManager
    //#    method: void fireDeleteWindow(Window, Window)
    //#    unanalyzed callee: void com.dmdirc.ui.interfaces.FrameManager:delWindow(FrameContainer, FrameContainer)
        }
    }
    //#WindowManager.java:371: end of method: void com.dmdirc.ui.WindowManager.fireDeleteWindow(Window, Window)
        
    /**
     * Proxy for selection events.
     */
    private static class WMSelectionListener implements SelectionListener {
    //#WindowManager.java:376: method: void com.dmdirc.ui.WindowManager$WMSelectionListener.com.dmdirc.ui.WindowManager$WMSelectionListener()
    //#WindowManager.java:376: end of method: void com.dmdirc.ui.WindowManager$WMSelectionListener.com.dmdirc.ui.WindowManager$WMSelectionListener()
    //#WindowManager.java:376: method: void com.dmdirc.ui.WindowManager$WMSelectionListener.com.dmdirc.ui.WindowManager$WMSelectionListener(WindowManager$1)
    //#input(void com.dmdirc.ui.WindowManager$WMSelectionListener(WindowManager$1)): this
    //#WindowManager.java:376: end of method: void com.dmdirc.ui.WindowManager$WMSelectionListener.com.dmdirc.ui.WindowManager$WMSelectionListener(WindowManager$1)

        /** {@inheritDoc} */
        @Override
        public void selectionChanged(final Window window) {
            for (SelectionListener listener : selListeners) {
    //#WindowManager.java:381: method: void com.dmdirc.ui.WindowManager$WMSelectionListener.selectionChanged(Window)
    //#input(void selectionChanged(Window)): __Dispatch_Table.selectionChanged(Lcom/dmdirc/ui/interfaces/Window;)V
    //#input(void selectionChanged(Window)): com/dmdirc/interfaces/SelectionListener.__Descendant_Table[com/dmdirc/interfaces/SelectionListener]
    //#input(void selectionChanged(Window)): com/dmdirc/interfaces/SelectionListener.__Descendant_Table[com/dmdirc/ui/WindowManager$WMSelectionListener]
    //#input(void selectionChanged(Window)): com/dmdirc/interfaces/SelectionListener.__Descendant_Table[others]
    //#input(void selectionChanged(Window)): com/dmdirc/interfaces/SelectionListener.__Dispatch_Table.selectionChanged(Lcom/dmdirc/ui/interfaces/Window;)V
    //#input(void selectionChanged(Window)): com/dmdirc/ui/WindowManager.selListeners
    //#input(void selectionChanged(Window)): window
    //#presumption(void selectionChanged(Window)): java.util.Iterator:next(...).__Tag@381 in {com/dmdirc/interfaces/SelectionListener, com/dmdirc/ui/WindowManager$WMSelectionListener}
    //#presumption(void selectionChanged(Window)): java.util.Iterator:next(...)@381 != null
    //#unanalyzed(void selectionChanged(Window)): Effects-of-calling:java.util.List:iterator
    //#unanalyzed(void selectionChanged(Window)): Effects-of-calling:java.util.Iterator:hasNext
    //#unanalyzed(void selectionChanged(Window)): Effects-of-calling:java.util.Iterator:next
    //#unanalyzed(void selectionChanged(Window)): Effects-of-calling:selectionChanged
    //#test_vector(void selectionChanged(Window)): java.util.Iterator:hasNext(...)@381: {0}, {1}
                listener.selectionChanged(window);
            }
        }
    //#WindowManager.java:384: end of method: void com.dmdirc.ui.WindowManager$WMSelectionListener.selectionChanged(Window)
        
    }

}    //#WindowManager.java:: end of class: com.dmdirc.ui.WindowManager
    //#output(com.dmdirc.ui.WindowManager$1__static_init): __Descendant_Table[com/dmdirc/ui/WindowManager$1]
    //#post(com.dmdirc.ui.WindowManager$1__static_init): __Descendant_Table[com/dmdirc/ui/WindowManager$1] == &__Dispatch_Table
    //#WindowManager.java:: end of method: com.dmdirc.ui.WindowManager$1.com.dmdirc.ui.WindowManager$1__static_init
    //#WindowManager.java:: end of class: com.dmdirc.ui.WindowManager$1
    //#output(com.dmdirc.ui.WindowManager$WMSelectionListener__static_init): __Descendant_Table[com/dmdirc/ui/WindowManager$WMSelectionListener]
    //#output(com.dmdirc.ui.WindowManager$WMSelectionListener__static_init): __Dispatch_Table.selectionChanged(Lcom/dmdirc/ui/interfaces/Window;)V
    //#output(com.dmdirc.ui.WindowManager$WMSelectionListener__static_init): com/dmdirc/interfaces/SelectionListener.__Descendant_Table[com/dmdirc/ui/WindowManager$WMSelectionListener]
    //#post(com.dmdirc.ui.WindowManager$WMSelectionListener__static_init): __Descendant_Table[com/dmdirc/ui/WindowManager$WMSelectionListener] == &__Dispatch_Table
    //#post(com.dmdirc.ui.WindowManager$WMSelectionListener__static_init): com/dmdirc/interfaces/SelectionListener.__Descendant_Table[com/dmdirc/ui/WindowManager$WMSelectionListener] == &__Dispatch_Table
    //#post(com.dmdirc.ui.WindowManager$WMSelectionListener__static_init): __Dispatch_Table.selectionChanged(Lcom/dmdirc/ui/interfaces/Window;)V == &selectionChanged
    //#WindowManager.java:: end of method: com.dmdirc.ui.WindowManager$WMSelectionListener.com.dmdirc.ui.WindowManager$WMSelectionListener__static_init
    //#WindowManager.java:: end of class: com.dmdirc.ui.WindowManager$WMSelectionListener
