File Source: MainFrame.java

         /* 
    P/P   *  Method: com.dmdirc.addons.ui_swing.MainFrame$1__static_init
          */
     1  /*
     2   * Copyright (c) 2006-2009 Chris Smith, Shane Mc Cormack, Gregory Holmes
     3   *
     4   * Permission is hereby granted, free of charge, to any person obtaining a copy
     5   * of this software and associated documentation files (the "Software"), to deal
     6   * in the Software without restriction, including without limitation the rights
     7   * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell
     8   * copies of the Software, and to permit persons to whom the Software is
     9   * furnished to do so, subject to the following conditions:
    10   *
    11   * The above copyright notice and this permission notice shall be included in
    12   * all copies or substantial portions of the Software.
    13   *
    14   * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND, EXPRESS OR
    15   * IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY,
    16   * FITNESS FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE
    17   * AUTHORS OR COPYRIGHT HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER
    18   * LIABILITY, WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING FROM,
    19   * OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE OR OTHER DEALINGS IN THE
    20   * SOFTWARE.
    21   */
    22  
    23  package com.dmdirc.addons.ui_swing;
    24  
    25  import com.dmdirc.addons.ui_swing.components.LoggingSwingWorker;
    26  import com.dmdirc.addons.ui_swing.components.desktopPane.DMDircDesktopPane;
    27  import com.dmdirc.FrameContainer;
    28  import com.dmdirc.Main;
    29  import com.dmdirc.ServerManager;
    30  import com.dmdirc.actions.ActionManager;
    31  import com.dmdirc.actions.CoreActionType;
    32  import com.dmdirc.config.IdentityManager;
    33  import com.dmdirc.interfaces.ConfigChangeListener;
    34  import com.dmdirc.ui.IconManager;
    35  import com.dmdirc.ui.WindowManager;
    36  import com.dmdirc.ui.interfaces.FrameManager;
    37  import com.dmdirc.ui.interfaces.FramemanagerPosition;
    38  import com.dmdirc.ui.interfaces.MainWindow;
    39  import com.dmdirc.ui.interfaces.Window;
    40  import com.dmdirc.addons.ui_swing.components.MenuBar;
    41  import com.dmdirc.addons.ui_swing.components.SnappingJSplitPane;
    42  import com.dmdirc.addons.ui_swing.components.statusbar.SwingStatusBar;
    43  import com.dmdirc.addons.ui_swing.framemanager.tree.TreeFrameManager;
    44  import com.dmdirc.ui.CoreUIUtils;
    45  import com.dmdirc.util.ReturnableThread;
    46  
    47  import java.awt.Dimension;
    48  import java.awt.event.WindowEvent;
    49  import java.awt.event.WindowFocusListener;
    50  import java.awt.event.WindowListener;
    51  
    52  import javax.swing.ImageIcon;
    53  import javax.swing.JComponent;
    54  import javax.swing.JDesktopPane;
    55  import javax.swing.JFrame;
    56  import javax.swing.JInternalFrame;
    57  import javax.swing.JOptionPane;
    58  import javax.swing.JPanel;
    59  import javax.swing.JSplitPane;
    60  import javax.swing.MenuSelectionManager;
    61  import javax.swing.WindowConstants;
    62  
    63  import net.miginfocom.swing.MigLayout;
    64  
    65  /**
    66   * The main application frame.
    67   */
         /* 
    P/P   *  Method: FrameManager access$500(MainFrame)
          * 
          *  Preconditions:
          *    x0 != null
          *    init'ed(x0.mainFrameManager)
          * 
          *  Postconditions:
          *    return_value == x0.mainFrameManager
          *    init'ed(return_value)
          */
    68  public final class MainFrame extends JFrame implements WindowListener,
    69          MainWindow, ConfigChangeListener, FrameManager {
    70  
    71      /** Logger to use. */
             /* 
    P/P       *  Method: com.dmdirc.addons.ui_swing.MainFrame__static_init
              * 
              *  Postconditions:
              *    init'ed(LOGGER)
              */
    72      private static final java.util.logging.Logger LOGGER =
    73              java.util.logging.Logger.getLogger(MainFrame.class.getName());
    74      /**
    75       * A version number for this class. It should be changed whenever the class
    76       * structure is changed (or anything else that would prevent serialized
    77       * objects being unserialized with the new class).
    78       */
    79      private static final long serialVersionUID = 9;
    80      /** Whether the internal frames are maximised or not. */
    81      private boolean maximised;
    82      /** The main application icon. */
    83      private ImageIcon imageIcon;
    84      /** The frame manager that's being used. */
    85      private FrameManager mainFrameManager;
    86      /** Dekstop pane. */
    87      private DMDircDesktopPane desktopPane;
    88      /** Main panel. */
    89      private JPanel frameManagerPanel;
    90      /** Frame manager position. */
    91      private FramemanagerPosition position;
    92      /** Show version? */
    93      private boolean showVersion;
    94      /** Menu bar. */
    95      private MenuBar menu;
    96      /** Exit code. */
    97      private int exitCode = 0;
    98      /** Swing Controller. */
    99      private SwingController controller;
   100      /** Status bar. */
   101      private SwingStatusBar statusBar;
   102  
   103      /**
   104       * Creates new form MainFrame.
   105       * 
   106       * @param controller Swing controller
   107       */
   108      protected MainFrame(final SwingController controller) {
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.MainFrame(SwingController)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@125 != null
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@127 != null
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@129 != null
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@131 != null
                  *    com.dmdirc.ui.IconManager:getIconManager(...)@115 != null
                  * 
                  *  Postconditions:
                  *    this.controller == controller
                  *    init'ed(this.controller)
                  *    init'ed(this.exitCode)
                  *    this.imageIcon == &new ImageIcon(MainFrame#1)
                  *    init'ed(this.showVersion)
                  *    new ImageIcon(MainFrame#1) num objects == 1
                  */
   109          super();
   110  
   111          this.controller = controller;
   112  
   113          initComponents();
   114  
   115          imageIcon =
   116                  new ImageIcon(IconManager.getIconManager().getImage("icon"));
   117          setIconImage(imageIcon.getImage());
   118  
   119          CoreUIUtils.centreWindow(this);
   120  
   121          setVisible(true);
   122  
   123          addWindowListener(this);
   124  
   125          showVersion = IdentityManager.getGlobalConfig().getOptionBool("ui",
   126                  "showversion");
   127          IdentityManager.getGlobalConfig().addChangeListener("ui", "lookandfeel",
   128                  this);
   129          IdentityManager.getGlobalConfig().addChangeListener("ui", "showversion",
   130                  this);
   131          IdentityManager.getGlobalConfig().addChangeListener("icon", "icon", this);
   132  
   133  
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.MainFrame$1(MainFrame)
                  */
   134          addWindowFocusListener(new WindowFocusListener() {
   135  
   136              /** {@inheritDoc} */
   137              @Override
   138              public void windowGainedFocus(WindowEvent e) {
   139                  //Ignore
                     /* 
    P/P               *  Method: void windowGainedFocus(WindowEvent)
                      */
   140              }
   141  
   142              /** {@inheritDoc} */
   143              @Override
   144              public void windowLostFocus(WindowEvent e) {
   145                  //TODO: Remove me when we switch to java7
                         /* 
    P/P                   *  Method: void windowLostFocus(WindowEvent)
                          * 
                          *  Presumptions:
                          *    javax.swing.MenuSelectionManager:defaultManager(...)@146 != null
                          */
   146                  MenuSelectionManager.defaultManager().clearSelectedPath();
   147              }
   148          });
   149  
   150          setTitle(getTitlePrefix());
   151      }
   152  
   153      /**
   154       * Returns the status bar for this frame.
   155       * 
   156       * @return Status bar
   157       */
   158      public SwingStatusBar getStatusBar() {
                 /* 
    P/P           *  Method: SwingStatusBar getStatusBar()
                  * 
                  *  Preconditions:
                  *    init'ed(this.statusBar)
                  * 
                  *  Postconditions:
                  *    return_value == this.statusBar
                  *    init'ed(return_value)
                  */
   159          return statusBar;
   160      }
   161  
   162      /**
   163       * Returns the size of the frame manager.
   164       *
   165       * @return Frame manager size.
   166       */
   167      public int getFrameManagerSize() {
                 /* 
    P/P           *  Method: int getFrameManagerSize()
                  * 
                  *  Presumptions:
                  *    com.dmdirc.util.ReturnableThread:getObject(...)@203 != null
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   168          return UIUtilities.invokeAndWait(new ReturnableThread<Integer>() {
   169  
   170              /** {@inheritDoc} */
   171              @Override
   172              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    this.frameManagerPanel != null
                          *    init'ed(this.position)
                          * 
                          *  Presumptions:
                          *    init'ed(com.dmdirc.ui.interfaces.FramemanagerPosition.LEFT)
                          *    init'ed(com.dmdirc.ui.interfaces.FramemanagerPosition.RIGHT)
                          */
   173                  if (position == FramemanagerPosition.LEFT ||
   174                          position == FramemanagerPosition.RIGHT) {
   175                      setObject(frameManagerPanel.getWidth());
   176                  } else {
   177                      setObject(frameManagerPanel.getHeight());
   178                  }
   179              }
   180          });
   181      }
   182  
   183      /** {@inheritDoc}. */
   184      @Override
   185      public ImageIcon getIcon() {
                 /* 
    P/P           *  Method: ImageIcon getIcon()
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   186          return UIUtilities.invokeAndWait(new ReturnableThread<ImageIcon>() {
   187  
   188              /** {@inheritDoc} */
   189              @Override
   190              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    init'ed(this.imageIcon)
                          */
   191                  setObject(imageIcon);
   192              }
   193          });
   194      }
   195  
   196      /**
   197       * Returns the window that is currently active.
   198       *
   199       * @return The active window
   200       */
   201      public Window getActiveFrame() {
                 /* 
    P/P           *  Method: Window getActiveFrame()
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   202          return UIUtilities.invokeAndWait(new ReturnableThread<Window>() {
   203  
   204              /** {@inheritDoc} */
   205              @Override
   206              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    this.desktopPane != null
                          */
   207                  setObject(desktopPane.getSelectedWindow());
   208              }
   209          });
   210      }
   211  
   212      /** {@inheritDoc}. */
   213      @Override
   214      public void setMaximised(final boolean max) {
   215          //Ignore
             /* 
    P/P       *  Method: void setMaximised(bool)
              */
   216      }
   217  
   218      /** {@inheritDoc}. */
   219      @Override
   220      public void setTitle(final String title) {
                 /* 
    P/P           *  Method: void setTitle(String)
                  * 
                  *  Preconditions:
                  *    init'ed(this.showVersion)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.util.ReturnableThread:getObject(...)@203 != null
                  * 
                  *  Test Vectors:
                  *    title: Addr_Set{null}, Inverse{null}
                  *    com.dmdirc.ui.interfaces.Window:isMaximum(...)@221: {0}, {1}
                  *    com.dmdirc.util.ReturnableThread:getObject(...)@203: Addr_Set{null}, Inverse{null}
                  */
   221          if (title != null && getActiveFrame() != null && getActiveFrame().isMaximum()) {
   222              super.setTitle(getTitlePrefix() + " - " + title);
   223          } else {
   224              super.setTitle(getTitlePrefix());
   225          }
   226      }
   227  
   228      /** {@inheritDoc}. */
   229      @Override
   230      public String getTitlePrefix() {
                 /* 
    P/P           *  Method: String getTitlePrefix()
                  * 
                  *  Preconditions:
                  *    init'ed(this.showVersion)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@232 != null
                  * 
                  *  Postconditions:
                  *    java.lang.StringBuilder:toString(...)._tainted == 0
                  *    return_value in Addr_Set{&amp;"DMDirc",&amp;java.lang.StringBuilder:toString(...)}
                  * 
                  *  Test Vectors:
                  *    this.showVersion: {0}, {1}
                  */
   231          if (showVersion) {
   232              return "DMDirc " + IdentityManager.getGlobalConfig().getOption(
   233                      "version", "version");
   234          } else {
   235              return "DMDirc";
   236          }
   237      }
   238  
   239      /** {@inheritDoc}. */
   240      @Override
   241      public boolean getMaximised() {
                 /* 
    P/P           *  Method: bool getMaximised()
                  * 
                  *  Presumptions:
                  *    com.dmdirc.util.ReturnableThread:getObject(...)@203 != null
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   242          return UIUtilities.invokeAndWait(new ReturnableThread<Boolean>() {
   243  
   244              /** {@inheritDoc}. */
   245              @Override
   246              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Presumptions:
                          *    com.dmdirc.util.ReturnableThread:getObject(...)@203 != null
                          *    getActiveFrame(...)@251 init'ed
                          * 
                          *  Test Vectors:
                          *    com.dmdirc.util.ReturnableThread:getObject(...)@203: Inverse{null}, Addr_Set{null}
                          */
   247                  final Window window = getActiveFrame();
   248                  if (window == null) {
   249                      setObject(false);
   250                  } else {
   251                      setObject(getActiveFrame().isMaximum());
   252                  }
   253              }
   254          });
   255      }
   256  
   257      /**
   258       * Returns the desktop pane for the frame.
   259       * 
   260       * @return JDesktopPane for the frame
   261       */
   262      public JDesktopPane getDesktopPane() {
                 /* 
    P/P           *  Method: JDesktopPane getDesktopPane()
                  * 
                  *  Preconditions:
                  *    init'ed(this.desktopPane)
                  * 
                  *  Postconditions:
                  *    return_value == this.desktopPane
                  *    init'ed(return_value)
                  */
   263          return desktopPane;
   264      }
   265  
   266      /** 
   267       * {@inheritDoc}.
   268       * 
   269       * @param windowEvent Window event
   270       */
   271      @Override
   272      public void windowOpened(final WindowEvent windowEvent) {
   273          //ignore
             /* 
    P/P       *  Method: void windowOpened(WindowEvent)
              */
   274      }
   275  
   276      /** 
   277       * {@inheritDoc}.
   278       * 
   279       * @param windowEvent Window event
   280       */
   281      @Override
   282      public void windowClosing(final WindowEvent windowEvent) {
                 /* 
    P/P           *  Method: void windowClosing(WindowEvent)
                  * 
                  *  Preconditions:
                  *    init'ed(this.exitCode)
                  * 
                  *  Postconditions:
                  *    this.exitCode == old this.exitCode
                  *    init'ed(this.exitCode)
                  */
   283          quit(exitCode);
   284      }
   285  
   286      /** 
   287       * {@inheritDoc}.
   288       * 
   289       * @param windowEvent Window event
   290       */
   291      @Override
   292      public void windowClosed(final WindowEvent windowEvent) {
                 /* 
    P/P           *  Method: void windowClosed(WindowEvent)
                  */
   293          new Thread(new Runnable() {
   294  
   295              /** {@inheritDoc} */
   296              @Override
   297              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    init'ed(this.exitCode)
                          */
   298                  Main.quit(exitCode);
   299              }
   300          }, "Quit thread").start();
   301      }
   302  
   303      /** 
   304       * {@inheritDoc}.
   305       * 
   306       * @param windowEvent Window event
   307       */
   308      @Override
   309      public void windowIconified(final WindowEvent windowEvent) {
                 /* 
    P/P           *  Method: void windowIconified(WindowEvent)
                  * 
                  *  Presumptions:
                  *    init'ed(com.dmdirc.actions.CoreActionType.CLIENT_MINIMISED)
                  */
   310          ActionManager.processEvent(CoreActionType.CLIENT_MINIMISED, null);
   311      }
   312  
   313      /** 
   314       * {@inheritDoc}.
   315       * 
   316       * @param windowEvent Window event
   317       */
   318      @Override
   319      public void windowDeiconified(final WindowEvent windowEvent) {
                 /* 
    P/P           *  Method: void windowDeiconified(WindowEvent)
                  * 
                  *  Presumptions:
                  *    init'ed(com.dmdirc.actions.CoreActionType.CLIENT_UNMINIMISED)
                  */
   320          ActionManager.processEvent(CoreActionType.CLIENT_UNMINIMISED, null);
   321      }
   322  
   323      /** 
   324       * {@inheritDoc}.
   325       * 
   326       * @param windowEvent Window event
   327       */
   328      @Override
   329      public void windowActivated(final WindowEvent windowEvent) {
   330          //ignore
             /* 
    P/P       *  Method: void windowActivated(WindowEvent)
              */
   331      }
   332  
   333      /** 
   334       * {@inheritDoc}.
   335       * 
   336       * @param windowEvent Window event
   337       */
   338      @Override
   339      public void windowDeactivated(final WindowEvent windowEvent) {
   340          //ignore
             /* 
    P/P       *  Method: void windowDeactivated(WindowEvent)
              */
   341      }
   342  
   343      /** Initialiases the frame managers. */
   344      private void initFrameManagers() {
                 /* 
    P/P           *  Method: void initFrameManagers()
                  */
   345          UIUtilities.invokeAndWait(new Runnable() {
   346  
   347              /** {@inheritDoc} */
   348              @Override
   349              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    init'ed(this.frameManagerPanel)
                          * 
                          *  Presumptions:
                          *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@350 != null
                          *    java.lang.Class:forName(...)@355 != null
                          *    java.lang.Class:getConstructor(...)@355 != null
                          *    java.lang.reflect.Constructor:newInstance(...)@355 != null
                          * 
                          *  Postconditions:
                          *    new TreeFrameManager(run#3) num objects <= 1
                          */
   350                  final String manager = IdentityManager.getGlobalConfig().
   351                          getOption("ui",
   352                          "framemanager");
   353  
   354                  try {
   355                      mainFrameManager = (FrameManager) Class.forName(manager).
   356                              getConstructor().newInstance();
   357                  } catch (Exception ex) {
   358                      // Throws craploads of exceptions and we want to handle them all
   359                      // the same way, so we might as well catch Exception
   360                      mainFrameManager = new TreeFrameManager();
   361                  }
   362  
   363  
   364                  WindowManager.addFrameManager(mainFrameManager);
   365                  mainFrameManager.setParent(frameManagerPanel);
   366  
   367                  WindowManager.addFrameManager(MainFrame.this);
   368              }
   369          });
   370      }
   371  
   372      /**
   373       * Initialises the components for this frame.
   374       */
   375      private void initComponents() {
                 /* 
    P/P           *  Method: void initComponents()
                  * 
                  *  Preconditions:
                  *    init'ed(com/dmdirc/addons/ui_swing/Apple.me)
                  *    init'ed(this.controller)
                  *    this.mainFrameManager != null
                  *    (soft) init'ed(com.dmdirc.addons.ui_swing.MainFrame$12__static_init.new int[](MainFrame$12__static_init#1)[...])
                  * 
                  *  Presumptions:
                  *    com.dmdirc.addons.ui_swing.MainFrame:getContentPane(...)@388 != null
                  *    com.dmdirc.addons.ui_swing.MainFrame:getContentPane(...)@390 != null
                  *    com.dmdirc.addons.ui_swing.MainFrame:getContentPane(...)@391 != null
                  *    com.dmdirc.ui.interfaces.FramemanagerPosition:values(...).length >= 1
                  * 
                  *  Postconditions:
                  *    com/dmdirc/addons/ui_swing/Apple.me == One-of{old com/dmdirc/addons/ui_swing/Apple.me, &amp;new Apple(getApple#1)}
                  *    com/dmdirc/addons/ui_swing/Apple.me != null
                  *    com/dmdirc/addons/ui_swing/Apple.me.menuBar == &amp;new MenuBar(initComponents#4)
                  *    this.menu == &amp;new MenuBar(initComponents#4)
                  *    this.desktopPane == &amp;new DMDircDesktopPane(initComponents#3)
                  *    this.frameManagerPanel == &amp;new JPanel(initComponents#2)
                  *    this.position != null
                  *    this.statusBar == &amp;new SwingStatusBar(initComponents#1)
                  *    new Apple(getApple#1) num objects <= 1
                  *    new ArrayList(Apple#1) num objects == new Apple(getApple#1) num objects
                  *    ...
                  */
   376          statusBar = new SwingStatusBar(controller, this);
   377          frameManagerPanel = new JPanel();
   378          desktopPane = new DMDircDesktopPane(this);
   379  
   380          initFrameManagers();
   381  
   382          menu = new MenuBar(controller, this);
   383          Apple.getApple().setMenuBar(menu);
   384          setJMenuBar(menu);
   385  
   386          setPreferredSize(new Dimension(800, 600));
   387  
   388          getContentPane().setLayout(new MigLayout(
   389                  "fill, ins rel, wrap 1, hidemode 2"));
   390          getContentPane().add(initSplitPane(), "grow, push");
   391          getContentPane().add(statusBar,
   392                  "hmax 20, wmax 100%-2*rel, wmin 100%-2*rel");
   393  
   394          setDefaultCloseOperation(WindowConstants.DO_NOTHING_ON_CLOSE);
   395  
   396          pack();
   397      }
   398  
   399      /**
   400       * Initialises the split pane.
   401       * 
   402       * @return Returns the initialised split pane
   403       */
   404      private JSplitPane initSplitPane() {
                 /* 
    P/P           *  Method: JSplitPane initSplitPane()
                  * 
                  *  Preconditions:
                  *    this.mainFrameManager != null
                  *    (soft) init'ed(com.dmdirc.addons.ui_swing.MainFrame$12__static_init.new int[](MainFrame$12__static_init#1)[...])
                  *    (soft) init'ed(this.desktopPane)
                  *    (soft) this.frameManagerPanel != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@229 != null
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@407 != null
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@432 != null
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@442 != null
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@451 != null
                  *    ...
                  * 
                  *  Postconditions:
                  *    return_value == &amp;new SnappingJSplitPane(initSplitPane#1)
                  *    this.position != null
                  *    new SnappingJSplitPane(initSplitPane#1) num objects == 1
                  *    return_value.leftComponentSnap == 1
                  *    return_value.config != null
                  *    return_value.snapDistance == 10
                  *    init'ed(return_value.useOneTouchExpandable)
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.addons.ui_swing.MainFrame$12__static_init.new int[](MainFrame$12__static_init#1)[...]: {1}, {2}, {3}, {4}, {-231..0, 5..232-1}
                  *    com.dmdirc.ui.interfaces.FrameManager:canPositionHorizontally(...)@420: {1}, {0}
                  *    com.dmdirc.ui.interfaces.FrameManager:canPositionVertically(...)@415: {1}, {0}
                  */
   405          final JSplitPane mainSplitPane =
   406                  new SnappingJSplitPane(SnappingJSplitPane.Orientation.HORIZONTAL);
   407          position =
   408                  FramemanagerPosition.getPosition(IdentityManager.getGlobalConfig().
   409                  getOption("ui", "framemanagerPosition"));
   410  
   411          if (position == FramemanagerPosition.UNKNOWN) {
   412              position = FramemanagerPosition.LEFT;
   413          }
   414  
   415          if (!mainFrameManager.canPositionVertically() &&
   416                  (position == FramemanagerPosition.LEFT ||
   417                  position == FramemanagerPosition.RIGHT)) {
   418              position = FramemanagerPosition.BOTTOM;
   419          }
   420          if (!mainFrameManager.canPositionHorizontally() &&
   421                  (position == FramemanagerPosition.TOP ||
   422                  position == FramemanagerPosition.BOTTOM)) {
   423              position = FramemanagerPosition.LEFT;
   424          }
   425  
                 /* 
    P/P           *  Method: com.dmdirc.addons.ui_swing.MainFrame$12__static_init
                  * 
                  *  Presumptions:
                  *    com.dmdirc.ui.interfaces.FramemanagerPosition.BOTTOM != null
                  *    com.dmdirc.ui.interfaces.FramemanagerPosition.LEFT != null
                  *    com.dmdirc.ui.interfaces.FramemanagerPosition.RIGHT != null
                  *    com.dmdirc.ui.interfaces.FramemanagerPosition.TOP != null
                  *    com.dmdirc.ui.interfaces.FramemanagerPosition:ordinal(...)@426 >= 0
                  *    ...
                  * 
                  *  Postconditions:
                  *    new int[](MainFrame$12__static_init#1) num objects == 1
                  */
   426          switch (position) {
   427              case TOP:
   428                  mainSplitPane.setTopComponent(frameManagerPanel);
   429                  mainSplitPane.setBottomComponent(desktopPane);
   430                  mainSplitPane.setResizeWeight(0.0);
   431                  mainSplitPane.setOrientation(JSplitPane.VERTICAL_SPLIT);
   432                  frameManagerPanel.setPreferredSize(new Dimension(
   433                          Integer.MAX_VALUE,
   434                          IdentityManager.getGlobalConfig().
   435                          getOptionInt("ui", "frameManagerSize")));
   436                  break;
   437              case LEFT:
   438                  mainSplitPane.setLeftComponent(frameManagerPanel);
   439                  mainSplitPane.setRightComponent(desktopPane);
   440                  mainSplitPane.setResizeWeight(0.0);
   441                  mainSplitPane.setOrientation(JSplitPane.HORIZONTAL_SPLIT);
   442                  frameManagerPanel.setPreferredSize(new Dimension(
   443                          IdentityManager.getGlobalConfig().getOptionInt("ui",
   444                          "frameManagerSize"), Integer.MAX_VALUE));
   445                  break;
   446              case BOTTOM:
   447                  mainSplitPane.setTopComponent(desktopPane);
   448                  mainSplitPane.setBottomComponent(frameManagerPanel);
   449                  mainSplitPane.setResizeWeight(1.0);
   450                  mainSplitPane.setOrientation(JSplitPane.VERTICAL_SPLIT);
   451                  frameManagerPanel.setPreferredSize(new Dimension(
   452                          Integer.MAX_VALUE,
   453                          IdentityManager.getGlobalConfig().
   454                          getOptionInt("ui", "frameManagerSize")));
   455                  break;
   456              case RIGHT:
   457                  mainSplitPane.setLeftComponent(desktopPane);
   458                  mainSplitPane.setRightComponent(frameManagerPanel);
   459                  mainSplitPane.setResizeWeight(1.0);
   460                  mainSplitPane.setOrientation(JSplitPane.HORIZONTAL_SPLIT);
   461                  frameManagerPanel.setPreferredSize(new Dimension(
   462                          IdentityManager.getGlobalConfig().getOptionInt("ui",
   463                          "frameManagerSize"), Integer.MAX_VALUE));
   464                  break;
   465              default:
   466                  break;
   467          }
   468  
   469          return mainSplitPane;
   470      }
   471  
   472      /** {@inheritDoc}. */
   473      @Override
   474      public void quit() {
                 /* 
    P/P           *  Method: void quit()
                  * 
                  *  Postconditions:
                  *    this.exitCode == One-of{old this.exitCode, 0}
                  */
   475          quit(0);
   476      }
   477  
   478      /** 
   479       * Exit code call to quit. 
   480       * 
   481       * @param exitCode Exit code
   482       */
   483      public void quit(final int exitCode) {
                 /* 
    P/P           *  Method: void quit(int)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@484 != null
                  * 
                  *  Postconditions:
                  *    this.exitCode == One-of{old this.exitCode, exitCode}
                  * 
                  *  Test Vectors:
                  *    exitCode: {-231..-1, 1..232-1}, {0}
                  *    com.dmdirc.config.ConfigManager:getOptionBool(...)@484: {0}, {1}
                  *    javax.swing.JOptionPane:showConfirmDialog(...)@484: {0}, {-231..-1, 1..232-1}
                  */
   484          if (exitCode == 0 && IdentityManager.getGlobalConfig().getOptionBool(
   485                  "ui", "confirmQuit") && JOptionPane.showConfirmDialog(this,
   486                  "You are about to quit DMDirc, are you sure?", "Quit confirm",
   487                  JOptionPane.YES_NO_OPTION,
   488                  JOptionPane.WARNING_MESSAGE) !=
   489                  JOptionPane.YES_OPTION) {
   490              return;
   491          }
   492  
   493          this.exitCode = exitCode;
   494  
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.MainFrame$8(MainFrame)
                  */
   495          new LoggingSwingWorker() {
   496  
   497              /** {@inheritDoc} */
   498              @Override
   499              protected Object doInBackground() throws Exception {
                         /* 
    P/P                   *  Method: Object doInBackground()
                          * 
                          *  Presumptions:
                          *    com.dmdirc.ServerManager:getServerManager(...)@501 != null
                          *    init'ed(com.dmdirc.actions.CoreActionType.CLIENT_CLOSING)
                          *    com.dmdirc.config.IdentityManager:getConfigIdentity(...)@503 != null
                          *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@501 != null
                          * 
                          *  Postconditions:
                          *    return_value == null
                          */
   500                  ActionManager.processEvent(CoreActionType.CLIENT_CLOSING, null);
   501                  ServerManager.getServerManager().closeAll(IdentityManager.
   502                          getGlobalConfig().getOption("general", "closemessage"));
   503                  IdentityManager.getConfigIdentity().setOption("ui",
   504                          "frameManagerSize",
   505                          String.valueOf(getFrameManagerSize()));
   506                  return null;
   507              }
   508  
   509              /** {@inheritDoc} */
   510              @Override
   511              protected void done() {
                         /* 
    P/P                   *  Method: void done()
                          */
   512                  super.done();
   513                  dispose();
   514              }
   515          }.execute();
   516      }
   517  
   518      /** {@inheritDoc} */
   519      @Override
   520      public void configChanged(final String domain, final String key) {
                 /* 
    P/P           *  Method: void configChanged(String, String)
                  * 
                  *  Preconditions:
                  *    (soft) this.controller != null
                  *    (soft) this.controller.windows != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.config.IdentityManager:getGlobalConfig(...)@525 != null
                  *    com.dmdirc.ui.IconManager:getIconManager(...)@530 != null
                  * 
                  *  Postconditions:
                  *    this.imageIcon == One-of{old this.imageIcon, &amp;new ImageIcon(configChanged#1)}
                  *    possibly_updated(this.showVersion)
                  *    new ImageIcon(configChanged#1) num objects <= 1
                  * 
                  *  Test Vectors:
                  *    java.lang.String:equals(...)@521: {0}, {1}
                  *    java.lang.String:equals(...)@522: {0}, {1}
                  */
   521          if ("ui".equals(domain)) {
   522              if ("lookandfeel".equals(key)) {
   523                  controller.updateLookAndFeel();
   524              } else {
   525                  showVersion = IdentityManager.getGlobalConfig().getOptionBool(
   526                          "ui",
   527                          "showversion");
   528              }
   529          } else {
   530              imageIcon = new ImageIcon(IconManager.getIconManager().getImage(
   531                      "icon"));
   532              setIconImage(imageIcon.getImage());
   533          }
   534      }
   535  
   536      /** {@inheritDoc}. */
   537      @Override
   538      public void setParent(final JComponent parent) {
   539          //Ignore
             /* 
    P/P       *  Method: void setParent(JComponent)
              */
   540      }
   541  
   542      /** {@inheritDoc}. */
   543      @Override
   544      public boolean canPositionVertically() {
                 /* 
    P/P           *  Method: bool canPositionVertically()
                  * 
                  *  Postconditions:
                  *    return_value == 1
                  */
   545          return true;
   546      }
   547  
   548      /** {@inheritDoc}. */
   549      @Override
   550      public boolean canPositionHorizontally() {
                 /* 
    P/P           *  Method: bool canPositionHorizontally()
                  * 
                  *  Postconditions:
                  *    return_value == 1
                  */
   551          return true;
   552      }
   553  
   554      /** {@inheritDoc}. */
   555      @Override
   556      public void addWindow(final FrameContainer window) {
                 /* 
    P/P           *  Method: void addWindow(FrameContainer)
                  */
   557          UIUtilities.invokeAndWait(new Runnable() {
   558  
   559              /** {@inheritDoc} */
   560              @Override
   561              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    this.desktopPane != null
                          * 
                          *  Presumptions:
                          *    com.dmdirc.addons.ui_swing.components.desktopPane.DMDircDesktopPane:getAllFrames(...).length@562 <= 232
                          *    com.dmdirc.addons.ui_swing.components.desktopPane.DMDircDesktopPane:getAllFrames(...)@562 != null
                          */
   562                  addWindow(window, desktopPane.getAllFrames().length - 1);
   563              }
   564          });
   565      }
   566  
   567      /**
   568       * Adds a window to this frame manager.
   569       * 
   570       * @param window The server to be added
   571       * @param index Index of the window to be added
   572       */
   573      public void addWindow(final FrameContainer window, final int index) {
                 /* 
    P/P           *  Method: void addWindow(FrameContainer, int)
                  */
   574          UIUtilities.invokeAndWait(new Runnable() {
   575  
   576              /** {@inheritDoc} */
   577              @Override
   578              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    this.desktopPane != null
                          *    this.val$window != null
                          */
   579                  final JInternalFrame frame = (JInternalFrame) window.getFrame();
   580  
   581                  // Add the frame
   582                  desktopPane.add(frame, index);
   583              }
   584          });
   585      }
   586  
   587      /** {@inheritDoc}. */
   588      @Override
   589      public void delWindow(final FrameContainer window) {
                 /* 
    P/P           *  Method: void delWindow(FrameContainer)
                  */
   590          UIUtilities.invokeAndWait(new Runnable() {
   591  
   592              /** {@inheritDoc} */
   593              @Override
   594              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    this.desktopPane != null
                          *    this.val$window != null
                          */
   595                  final JInternalFrame frame = (JInternalFrame) window.getFrame();
   596  
   597                  desktopPane.remove(frame);
   598              }
   599          });
   600      }
   601  
   602      /** {@inheritDoc}. */
   603      @Override
   604      public void addWindow(final FrameContainer parent,
   605              final FrameContainer window) {
                 /* 
    P/P           *  Method: void addWindow(FrameContainer, FrameContainer)
                  */
   606          addWindow(window);
   607      }
   608  
   609      /** {@inheritDoc}. */
   610      @Override
   611      public void delWindow(final FrameContainer parent,
   612              final FrameContainer window) {
                 /* 
    P/P           *  Method: void delWindow(FrameContainer, FrameContainer)
                  */
   613          delWindow(window);
   614      }
   615  }








SofCheck Inspector Build Version : 2.17854
MainFrame.java 2009-Jun-25 01:54:24
MainFrame.class 2009-Sep-02 17:04:17
MainFrame$1.class 2009-Sep-02 17:04:17
MainFrame$10.class 2009-Sep-02 17:04:17
MainFrame$11.class 2009-Sep-02 17:04:17
MainFrame$12.class 2009-Sep-02 17:04:17
MainFrame$2.class 2009-Sep-02 17:04:17
MainFrame$3.class 2009-Sep-02 17:04:17
MainFrame$4.class 2009-Sep-02 17:04:17
MainFrame$5.class 2009-Sep-02 17:04:17
MainFrame$6.class 2009-Sep-02 17:04:17
MainFrame$7.class 2009-Sep-02 17:04:17
MainFrame$8.class 2009-Sep-02 17:04:17
MainFrame$9.class 2009-Sep-02 17:04:17