File Source: InputTextFrame.java

         /* 
    P/P   *  Method: com.dmdirc.addons.ui_swing.components.frames.InputTextFrame__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  package com.dmdirc.addons.ui_swing.components.frames;
    23  
    24  import com.dmdirc.WritableFrameContainer;
    25  import com.dmdirc.addons.ui_swing.SwingController;
    26  import com.dmdirc.commandparser.PopupManager;
    27  import com.dmdirc.commandparser.PopupMenu;
    28  import com.dmdirc.commandparser.PopupMenuItem;
    29  import com.dmdirc.commandparser.PopupType;
    30  import com.dmdirc.config.ConfigManager;
    31  import com.dmdirc.interfaces.AwayStateListener;
    32  import com.dmdirc.logger.ErrorLevel;
    33  import com.dmdirc.logger.Logger;
    34  import com.dmdirc.ui.input.InputHandler;
    35  import com.dmdirc.ui.interfaces.InputWindow;
    36  import com.dmdirc.addons.ui_swing.UIUtilities;
    37  import com.dmdirc.addons.ui_swing.actions.CopyAction;
    38  import com.dmdirc.addons.ui_swing.actions.CutAction;
    39  import com.dmdirc.addons.ui_swing.actions.InputTextFramePasteAction;
    40  import com.dmdirc.addons.ui_swing.dialogs.paste.PasteDialog;
    41  import com.dmdirc.addons.ui_swing.actions.CommandAction;
    42  import com.dmdirc.addons.ui_swing.components.SwingInputField;
    43  
    44  import java.awt.BorderLayout;
    45  import java.awt.Point;
    46  import java.awt.Toolkit;
    47  import java.awt.datatransfer.DataFlavor;
    48  import java.awt.datatransfer.UnsupportedFlavorException;
    49  import java.awt.event.MouseEvent;
    50  import java.io.IOException;
    51  
    52  import javax.swing.JComponent;
    53  import javax.swing.JLabel;
    54  import javax.swing.JMenu;
    55  import javax.swing.JMenuItem;
    56  import javax.swing.JPanel;
    57  import javax.swing.JPopupMenu;
    58  import javax.swing.JSeparator;
    59  import javax.swing.KeyStroke;
    60  
    61  import net.miginfocom.layout.PlatformDefaults;
    62  
    63  /**
    64   * Frame with an input field.
    65   */
         /* 
    P/P   *  Method: FrameContainer getContainer()
          * 
          *  Postconditions:
          *    init'ed(return_value)
          */
    66  public abstract class InputTextFrame extends TextFrame implements InputWindow,
    67          AwayStateListener {
    68  
    69      /**
    70       * A version number for this class. It should be changed whenever the class
    71       * structure is changed (or anything else that would prevent serialized
    72       * objects being unserialized with the new class).
    73       */
    74      private static final long serialVersionUID = 2;
    75      /** Input field panel. */
    76      protected JPanel inputPanel;
    77      /** Away label. */
    78      protected JLabel awayLabel;
    79      /** The InputHandler for our input field. */
    80      private InputHandler inputHandler;
    81      /** Frame input field. */
    82      private SwingInputField inputField;
    83      /** Popupmenu for this frame. */
    84      private JPopupMenu inputFieldPopup;
    85      /** Nick popup menu. */
    86      protected JPopupMenu nickPopup;
    87  
    88      /**
    89       * Creates a new instance of InputFrame.
    90       *
    91       * @param owner WritableFrameContainer owning this frame.
    92       * @param controller Swing controller
    93       */
    94      public InputTextFrame(final WritableFrameContainer owner, final SwingController controller) {
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.components.frames.InputTextFrame(WritableFrameContainer, SwingController)
                  * 
                  *  Preconditions:
                  *    owner != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.WritableFrameContainer:getConfigManager(...)@99 != null
                  *    com.dmdirc.WritableFrameContainer:getServer(...)@114 != null
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:getContainer(...)@187 != null
                  * 
                  *  Postconditions:
                  *    this.awayLabel == &new JLabel(initComponents#3)
                  *    this.inputField == &new SwingInputField(initComponents#1)
                  *    this.inputFieldPopup == &new JPopupMenu(initPopupMenu#1)
                  *    this.inputPanel == &new JPanel(initComponents#4)
                  *    this.nickPopup == &new JPopupMenu(initComponents#2)
                  *    new JLabel(SwingInputField#3) num objects == 1
                  *    new JLabel(SwingInputField#4) num objects == 1
                  *    new JLabel(initComponents#3) num objects == 1
                  *    new JPanel(initComponents#4) num objects == 1
                  *    new JPopupMenu(initComponents#2) num objects == 1
                  *    ...
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.WritableFrameContainer:getServer(...)@113: Addr_Set{null}, Inverse{null}
                  */
    95          super(owner, controller);
    96  
    97          initComponents();
    98  
    99          final ConfigManager config = owner.getConfigManager();
   100  
   101          getInputField().setBackground(config.getOptionColour(
   102                  "ui", "inputbackgroundcolour",
   103                  "ui", "backgroundcolour"));
   104          getInputField().setForeground(config.getOptionColour(
   105                  "ui", "inputforegroundcolour",
   106                  "ui", "foregroundcolour"));
   107          getInputField().setCaretColor(config.getOptionColour(
   108                  "ui", "inputforegroundcolour",
   109                  "ui", "foregroundcolour"));
   110  
   111          config.addChangeListener("ui", "inputforegroundcolour", this);
   112          config.addChangeListener("ui", "inputbackgroundcolour", this);
   113          if (getContainer().getServer() != null) {
   114              getContainer().getServer().addAwayStateListener(this);
   115          }
   116      }
   117  
   118      /** {@inheritDoc} */
   119      @Override
   120      public void open() {
                 /* 
    P/P           *  Method: void open()
                  * 
                  *  Preconditions:
                  *    this.inputField != null
                  *    (soft) this.awayLabel != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.WritableFrameContainer:getServer(...)@124 != null
                  *    com.dmdirc.addons.ui_swing.components.frames.InputTextFrame:getConfigManager(...)@122 != null
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:getContainer(...)@187 != null
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.WritableFrameContainer:getServer(...)@122: Addr_Set{null}, Inverse{null}
                  *    com.dmdirc.config.ConfigManager:getOptionBool(...)@122: {0}, {1}
                  */
   121          super.open();
   122          if (getConfigManager().getOptionBool("ui", "awayindicator") && getContainer().
   123                  getServer() != null) {
   124              awayLabel.setVisible(getContainer().getServer().isAway());
   125          }
   126  
   127          inputField.requestFocusInWindow();
   128      }
   129  
   130      /**
   131       * Initialises the components for this frame.
   132       */
   133      private void initComponents() {
                 /* 
    P/P           *  Method: void initComponents()
                  * 
                  *  Presumptions:
                  *    (int) (net.miginfocom.layout.UnitValue:getValue(...)@146) in {-231..232-1}
                  *    net.miginfocom.layout.PlatformDefaults:getUnitValueX(...)@146 != null
                  * 
                  *  Postconditions:
                  *    this.awayLabel == &new JLabel(initComponents#3)
                  *    this.inputField == &new SwingInputField(initComponents#1)
                  *    this.inputFieldPopup == &new JPopupMenu(initPopupMenu#1)
                  *    this.inputPanel == &new JPanel(initComponents#4)
                  *    this.nickPopup == &new JPopupMenu(initComponents#2)
                  *    new JLabel(SwingInputField#3) num objects == 1
                  *    new JLabel(SwingInputField#4) num objects == 1
                  *    new JLabel(initComponents#3) num objects == 1
                  *    new JPanel(initComponents#4) num objects == 1
                  *    new JPopupMenu(initComponents#2) num objects == 1
                  *    ...
                  */
   134          setInputField(new SwingInputField());
   135  
   136          getInputField().addKeyListener(this);
   137          getInputField().addMouseListener(this);
   138  
   139          initPopupMenu();
   140          nickPopup = new JPopupMenu();
   141  
   142          awayLabel = new JLabel();
   143          awayLabel.setText("(away)");
   144          awayLabel.setVisible(false);
   145  
   146          inputPanel = new JPanel(new BorderLayout(
   147                  (int) PlatformDefaults.getUnitValueX("related").getValue(),
   148                  (int) PlatformDefaults.getUnitValueX("related").getValue()));
   149          inputPanel.add(awayLabel, BorderLayout.LINE_START);
   150          inputPanel.add(inputField, BorderLayout.CENTER);
   151  
   152          initInputField();
   153      }
   154  
   155      /** Initialises the popupmenu. */
   156      private void initPopupMenu() {
                 /* 
    P/P           *  Method: void initPopupMenu()
                  * 
                  *  Preconditions:
                  *    this.inputField != null
                  * 
                  *  Postconditions:
                  *    this.inputFieldPopup == &new JPopupMenu(initPopupMenu#1)
                  *    new JPopupMenu(initPopupMenu#1) num objects == 1
                  */
   157          inputFieldPopup = new JPopupMenu();
   158  
   159          inputFieldPopup.add(new CutAction(getInputField().getTextField()));
   160          inputFieldPopup.add(new CopyAction(getInputField().getTextField()));
   161          inputFieldPopup.add(new InputTextFramePasteAction(this));
   162          inputFieldPopup.setOpaque(true);
   163          inputFieldPopup.setLightWeightPopupEnabled(true);
   164      }
   165  
   166      /**
   167       * Initialises the input field.
   168       */
   169      private void initInputField() {
                 /* 
    P/P           *  Method: void initInputField()
                  * 
                  *  Preconditions:
                  *    this.inputField != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.addons.ui_swing.components.SwingInputField:getActionMap(...)@172 != null
                  *    com.dmdirc.addons.ui_swing.components.SwingInputField:getInputMap(...)@174 != null
                  *    com.dmdirc.addons.ui_swing.components.SwingInputField:getInputMap(...)@176 != null
                  *    com.dmdirc.util.ReturnableThread:getObject(...)@203 != null
                  */
   170          UIUtilities.addUndoManager(getInputField().getTextField());
   171  
   172          getInputField().getActionMap().put("paste",
   173                  new InputTextFramePasteAction(this));
   174          getInputField().getInputMap(WHEN_FOCUSED).put(KeyStroke.getKeyStroke("shift INSERT"),
   175                  "paste");
   176          getInputField().getInputMap(WHEN_FOCUSED).put(KeyStroke.getKeyStroke("ctrl V"),
   177                  "paste");
   178      }
   179  
   180      /**
   181       * Returns the container associated with this frame.
   182       *
   183       * @return This frame's container.
   184       */
   185      @Override
   186      public WritableFrameContainer getContainer() {
                 /* 
    P/P           *  Method: WritableFrameContainer getContainer()
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   187          return (WritableFrameContainer) super.getContainer();
   188      }
   189  
   190      /**
   191       * Returns the input handler associated with this frame.
   192       *
   193       * @return Input handlers for this frame
   194       */
   195      @Override
   196      public final InputHandler getInputHandler() {
                 /* 
    P/P           *  Method: InputHandler getInputHandler()
                  * 
                  *  Preconditions:
                  *    init'ed(this.inputHandler)
                  * 
                  *  Postconditions:
                  *    return_value == this.inputHandler
                  *    init'ed(return_value)
                  */
   197          return inputHandler;
   198      }
   199  
   200      /**
   201       * Sets the input handler for this frame.
   202       *
   203       * @param newInputHandler input handler to set for this frame
   204       */
   205      public final void setInputHandler(final InputHandler newInputHandler) {
                 /* 
    P/P           *  Method: void setInputHandler(InputHandler)
                  * 
                  *  Preconditions:
                  *    newInputHandler != null
                  *    init'ed(this.inputField)
                  * 
                  *  Postconditions:
                  *    this.inputHandler == newInputHandler
                  *    this.inputHandler != null
                  */
   206          this.inputHandler = newInputHandler;
   207          inputHandler.addValidationListener(inputField);
   208      }
   209  
   210      /**
   211       * Returns the input field for this frame.
   212       *
   213       * @return SwingInputField input field for the frame.
   214       */
   215      public final SwingInputField getInputField() {
                 /* 
    P/P           *  Method: SwingInputField getInputField()
                  * 
                  *  Preconditions:
                  *    init'ed(this.inputField)
                  * 
                  *  Postconditions:
                  *    return_value == this.inputField
                  *    init'ed(return_value)
                  */
   216          return inputField;
   217      }
   218  
   219      /**
   220       * Sets the frames input field.
   221       *
   222       * @param newInputField new input field to use
   223       */
   224      protected final void setInputField(final SwingInputField newInputField) {
                 /* 
    P/P           *  Method: void setInputField(SwingInputField)
                  * 
                  *  Postconditions:
                  *    this.inputField == newInputField
                  *    init'ed(this.inputField)
                  */
   225          this.inputField = newInputField;
   226      }
   227  
   228      /**
   229       * Returns the away label for this server connection.
   230       *
   231       * @return JLabel away label
   232       */
   233      public JLabel getAwayLabel() {
                 /* 
    P/P           *  Method: JLabel getAwayLabel()
                  * 
                  *  Preconditions:
                  *    init'ed(this.awayLabel)
                  * 
                  *  Postconditions:
                  *    return_value == this.awayLabel
                  *    init'ed(return_value)
                  */
   234          return awayLabel;
   235      }
   236  
   237      /**
   238       * Sets the away indicator on or off.
   239       *
   240       * @param awayState away state
   241       */
   242      @Override
   243      public void setAwayIndicator(final boolean awayState) {
                 /* 
    P/P           *  Method: void setAwayIndicator(bool)
                  * 
                  *  Preconditions:
                  *    (soft) this.awayLabel != null
                  *    (soft) this.inputPanel != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.addons.ui_swing.components.frames.InputTextFrame:getConfigManager(...)@244 != null
                  * 
                  *  Test Vectors:
                  *    awayState: {1}, {0}
                  */
   244          final boolean awayIndicator = getConfigManager().
   245                  getOptionBool("ui", "awayindicator");
   246          if (awayIndicator || !awayState) {
   247              if (awayState) {
   248                  inputPanel.add(awayLabel, BorderLayout.LINE_START);
   249                  awayLabel.setVisible(true);
   250              } else {
   251                  awayLabel.setVisible(false);
   252              }
   253          }
   254      }
   255  
   256      /**
   257       * Checks for url's, channels and nicknames. {@inheritDoc}
   258       */
   259      @Override
   260      public void mouseClicked(final MouseEvent mouseEvent) {
                 /* 
    P/P           *  Method: void mouseClicked(MouseEvent)
                  * 
                  *  Preconditions:
                  *    mouseEvent != null
                  *    (soft) this.inputField != null
                  * 
                  *  Postconditions:
                  *    possibly_updated(this.inputFieldPopup)
                  *    new JPopupMenu(initPopupMenu#1) num objects <= 1
                  */
   261          if (mouseEvent.getSource() == getTextPane()) {
   262              processMouseEvent(mouseEvent);
   263          }
   264          super.mouseClicked(mouseEvent);
   265      }
   266  
   267      /**
   268       * Not needed for this class. {@inheritDoc}
   269       */
   270      @Override
   271      public void mousePressed(final MouseEvent mouseEvent) {
                 /* 
    P/P           *  Method: void mousePressed(MouseEvent)
                  * 
                  *  Preconditions:
                  *    mouseEvent != null
                  *    (soft) this.inputField != null
                  * 
                  *  Postconditions:
                  *    possibly_updated(this.inputFieldPopup)
                  *    new JPopupMenu(initPopupMenu#1) num objects <= 1
                  */
   272          processMouseEvent(mouseEvent);
   273          super.mousePressed(mouseEvent);
   274      }
   275  
   276      /**
   277       * Not needed for this class. {@inheritDoc}
   278       */
   279      @Override
   280      public void mouseReleased(final MouseEvent mouseEvent) {
                 /* 
    P/P           *  Method: void mouseReleased(MouseEvent)
                  * 
                  *  Preconditions:
                  *    mouseEvent != null
                  *    (soft) this.inputField != null
                  * 
                  *  Postconditions:
                  *    possibly_updated(this.inputFieldPopup)
                  *    new JPopupMenu(initPopupMenu#1) num objects <= 1
                  */
   281          processMouseEvent(mouseEvent);
   282          super.mouseReleased(mouseEvent);
   283      }
   284  
   285      /**
   286       * Processes every mouse button event to check for a popup trigger.
   287       *
   288       * @param e mouse event
   289       */
   290      @Override
   291      public void processMouseEvent(final MouseEvent e) {
                 /* 
    P/P           *  Method: void processMouseEvent(MouseEvent)
                  * 
                  *  Preconditions:
                  *    e != null
                  *    (soft) this.inputField != null
                  * 
                  *  Presumptions:
                  *    (int) (java.awt.Point:getX(...)@297) in {-231..232-1}
                  *    (int) (net.miginfocom.layout.UnitValue:getValue(...)@297) + (int) (java.awt.Point:getY(...)@297) + com.dmdirc.addons.ui_swing.textpane.TextPane:getHeight(...)@297 in range
                  *    (int) (net.miginfocom.layout.UnitValue:getValue(...)@297) + (int) (java.awt.Point:getY(...)@297) + com.dmdirc.addons.ui_swing.textpane.TextPane:getHeight(...)@297 in {-231..232-1}
                  *    com.dmdirc.addons.ui_swing.components.frames.InputTextFrame:getTextPane(...)@297 != null
                  *    net.miginfocom.layout.PlatformDefaults:getUnitValueX(...)@297 != null
                  * 
                  *  Postconditions:
                  *    this.inputFieldPopup == One-of{old this.inputFieldPopup, &amp;new JPopupMenu(initPopupMenu#1)}
                  *    new JPopupMenu(initPopupMenu#1) num objects <= 1
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.addons.ui_swing.components.SwingInputField:getMousePosition(...)@293: Addr_Set{null}, Inverse{null}
                  *    java.awt.event.MouseEvent:isPopupTrigger(...)@292: {0}, {1}
                  */
   292          if (e.isPopupTrigger() && e.getSource() == getInputField()) {
   293              final Point point = getInputField().getMousePosition();
   294  
   295              if (point != null) {
   296                  initPopupMenu();
   297                  inputFieldPopup.show(this, (int) point.getX(),
   298                          (int) point.getY() + getTextPane().getHeight() +
   299                          (int) PlatformDefaults.getUnitValueX("related").getValue());
   300              }
   301          }
   302          super.processMouseEvent(e);
   303      }
   304  
   305      /** Checks and pastes text. */
   306      public void doPaste() {
                 /* 
    P/P           *  Method: void doPaste()
                  * 
                  *  Preconditions:
                  *    (soft) this.inputField != null
                  * 
                  *  Presumptions:
                  *    init'ed(com.dmdirc.logger.ErrorLevel.LOW)
                  *    java.awt.Toolkit:getDefaultToolkit(...)@310 != null
                  *    java.awt.Toolkit:getDefaultToolkit(...)@321 != null
                  *    java.awt.Toolkit:getSystemClipboard(...)@310 != null
                  *    java.awt.Toolkit:getSystemClipboard(...)@321 != null
                  *    ...
                  * 
                  *  Test Vectors:
                  *    java.awt.datatransfer.Clipboard:isDataFlavorAvailable(...)@310: {1}, {0}
                  */
   307          String clipboard = null;
   308  
   309          try {
   310              if (!Toolkit.getDefaultToolkit().getSystemClipboard().
   311                      isDataFlavorAvailable(DataFlavor.stringFlavor)) {
   312                  return;
   313              }
   314          } catch (IllegalStateException ex) {
   315              Logger.userError(ErrorLevel.LOW, "Unable to paste from clipboard.");
   316              return;
   317          }
   318  
   319          try {
   320              //get the contents of the input field and combine it with the clipboard
   321              clipboard = (String) Toolkit.getDefaultToolkit().
   322                      getSystemClipboard().getData(DataFlavor.stringFlavor);
   323              doPaste(clipboard);
   324          } catch (IOException ex) {
   325              Logger.userError(ErrorLevel.LOW, "Unable to get clipboard contents: " +
   326                      ex.getMessage());
   327          } catch (UnsupportedFlavorException ex) {
   328              Logger.appError(ErrorLevel.LOW, "Unable to get clipboard contents",
   329                      ex);
   330          }
   331      }
   332  
   333      /**
   334       * Pastes the specified content into the input area.
   335       *
   336       * @param clipboard The contents of the clipboard to be pasted
   337       * @since 0.6.3m1
   338       */
   339      protected void doPaste(final String clipboard) {
   340          String[] clipboardLines;
   341          //check theres something to paste
                 /* 
    P/P           *  Method: void doPaste(String)
                  * 
                  *  Preconditions:
                  *    this.inputField != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.addons.ui_swing.components.frames.InputTextFrame:getConfigManager(...)@347 != null
                  *    com.dmdirc.addons.ui_swing.components.frames.InputTextFrame:getController(...)@352 != null
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:getContainer(...)@187 != null
                  *    com.dmdirc.util.ReturnableThread:getObject(...)@203 != null
                  *    getSplitLine(...).length <= 232-1
                  * 
                  *  Test Vectors:
                  *    clipboard: Addr_Set{null}, Inverse{null}
                  *    getSplitLine(...).length: {0,1}, {2..232-1}
                  */
   342          if (clipboard != null && (clipboardLines = getSplitLine(clipboard)).length > 1) {
   343              final int caretPosition = getInputField().getCaretPosition();
   344              final String inputFieldText = getInputField().getText();
   345              final String text = inputFieldText.substring(0, caretPosition) + clipboard + inputFieldText.substring(caretPosition);
   346              //check the limit
   347              final int pasteTrigger = getConfigManager().getOptionInt("ui",
   348                      "pasteProtectionLimit");
   349              //check whether the number of lines is over the limit
   350              if (getContainer().getNumLines(text) > pasteTrigger) {
   351                  //show the multi line paste dialog
   352                  new PasteDialog(this, text, getController().getMainFrame()).setVisible(true);
   353                  inputField.setText("");
   354              } else {
   355                  //send the lines
   356                  for (String clipboardLine : clipboardLines) {
   357                      getContainer().sendLine(clipboardLine);
   358                  }
   359              }
   360          } else {
   361              inputField.replaceSelection(clipboard);
   362          }
   363      }
   364  
   365      /**
   366       * Splits the line on all line endings.
   367       *
   368       * @param line Line that will be split
   369       *
   370       * @return Split line array
   371       */
   372      private String[] getSplitLine(final String line) {
                 /* 
    P/P           *  Method: String[] getSplitLine(String)
                  * 
                  *  Preconditions:
                  *    line != null
                  * 
                  *  Postconditions:
                  *    java.lang.String:split(...)._tainted == 0
                  *    return_value == &amp;java.lang.String:split(...)
                  */
   373          return line.replace("\r\n", "\n").replace('\r', '\n').split("\n");
   374      }
   375  
   376      /** {@inheritDoc} */
   377      @Override
   378      public void configChanged(final String domain, final String key) {
                 /* 
    P/P           *  Method: void configChanged(String, String)
                  * 
                  *  Preconditions:
                  *    (soft) init'ed(this.inputField)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.addons.ui_swing.components.frames.InputTextFrame:getConfigManager(...)@385 != null
                  *    com.dmdirc.addons.ui_swing.components.frames.InputTextFrame:getConfigManager(...)@390 != null
                  *    com.dmdirc.addons.ui_swing.components.frames.InputTextFrame:getConfigManager(...)@393 != null
                  * 
                  *  Test Vectors:
                  *    this.inputField: Addr_Set{null}, Inverse{null}
                  *    com.dmdirc.addons.ui_swing.components.frames.InputTextFrame:getConfigManager(...)@381: Addr_Set{null}, Inverse{null}
                  *    java.lang.String:equals(...)@381: {0}, {1}
                  *    java.lang.String:equals(...)@383: {1}, {0}
                  *    java.lang.String:equals(...)@383: {0}, {1}
                  *    java.lang.String:equals(...)@388: {1}, {0}
                  *    java.lang.String:equals(...)@388: {0}, {1}
                  */
   379          super.configChanged(domain, key);
   380  
   381          if ("ui".equals(domain) && getInputField() != null &&
   382                  getConfigManager() != null) {
   383              if ("inputbackgroundcolour".equals(key) ||
   384                      "backgroundcolour".equals(key)) {
   385                  getInputField().setBackground(getConfigManager().getOptionColour(
   386                          "ui", "inputbackgroundcolour",
   387                          "ui", "backgroundcolour"));
   388              } else if ("inputforegroundcolour".equals(key) ||
   389                      "foregroundcolour".equals(key)) {
   390                  getInputField().setForeground(getConfigManager().getOptionColour(
   391                          "ui", "inputforegroundcolour",
   392                          "ui", "foregroundcolour"));
   393                  getInputField().setCaretColor(getConfigManager().getOptionColour(
   394                          "ui", "inputforegroundcolour",
   395                          "ui", "foregroundcolour"));
   396  
   397              }
   398          }
   399      }
   400  
   401      /** 
   402       * Popuplates the nicklist popup. 
   403       *
   404       * @param nickname Nickname for the popup
   405       */
   406      protected final void popuplateNicklistPopup(final String nickname) {
                 /* 
    P/P           *  Method: void popuplateNicklistPopup(String)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.commandparser.PopupManager:getMenu(...)@407 != null
                  *    init'ed(com.dmdirc.commandparser.PopupType.CHAN_NICK)
                  * 
                  *  Postconditions:
                  *    this.nickPopup == &amp;new JPopupMenu(popuplateNicklistPopup#1)
                  *    new JPopupMenu(popuplateNicklistPopup#1) num objects == 1
                  */
   407          final PopupMenu popups = PopupManager.getMenu(PopupType.CHAN_NICK,
   408                  getConfigManager());
   409  
   410          nickPopup = (JPopupMenu) populatePopupMenu(new JPopupMenu(), popups,
   411                  nickname);
   412      }
   413  
   414      /**
   415       * Populates the specified popupmenu
   416       * 
   417       * @param menu Menu component
   418       * @param popup Popup to get info from
   419       * @param arguments Arguments for the command
   420       * 
   421       * @return Populated popup
   422       */
   423      private JComponent populatePopupMenu(final JComponent menu,
   424              final PopupMenu popup, final Object... arguments) {
                 /* 
    P/P           *  Method: JComponent populatePopupMenu(JComponent, PopupMenu, Object[])
                  * 
                  *  Preconditions:
                  *    popup != null
                  *    (soft) menu != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.commandparser.PopupMenu:getItems(...)@425 != null
                  *    com.dmdirc.commandparser.PopupMenuItem:getSubMenu(...)@429 != null
                  *    java.util.Iterator:next(...)@425 != null
                  * 
                  *  Postconditions:
                  *    return_value == menu
                  *    return_value != null
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.commandparser.PopupMenuItem:isDivider(...)@426: {0}, {1}
                  *    com.dmdirc.commandparser.PopupMenuItem:isSubMenu(...)@428: {0}, {1}
                  *    java.util.Iterator:hasNext(...)@425: {0}, {1}
                  */
   425          for (PopupMenuItem menuItem : popup.getItems()) {
   426              if (menuItem.isDivider()) {
   427                  menu.add(new JSeparator());
   428              } else if (menuItem.isSubMenu()) {
   429                  menu.add(populatePopupMenu(new JMenu(menuItem.getName()),
   430                          menuItem.getSubMenu(), arguments));
   431              } else {
   432                  menu.add(new JMenuItem(new CommandAction(getCommandParser(),
   433                          this, menuItem.getName(), menuItem.getCommand(arguments))));
   434              }
   435          }
   436          return menu;
   437      }
   438  
   439      /** Request input field focus. */
   440      public void requestInputFieldFocus() {
                 /* 
    P/P           *  Method: void requestInputFieldFocus()
                  * 
                  *  Preconditions:
                  *    init'ed(this.inputField)
                  * 
                  *  Test Vectors:
                  *    this.inputField: Addr_Set{null}, Inverse{null}
                  */
   441          if (inputField != null) {
   442              inputField.requestFocusInWindow();
   443          }
   444      }
   445  
   446      /** {@inheritDoc} */
   447      @Override
   448      public void onAway(final String reason) {
                 /* 
    P/P           *  Method: void onAway(String)
                  * 
                  *  Preconditions:
                  *    (soft) this.awayLabel != null
                  *    (soft) this.inputPanel != null
                  */
   449          setAwayIndicator(true);
   450      }
   451  
   452      /** {@inheritDoc} */
   453      @Override
   454      public void onBack() {
                 /* 
    P/P           *  Method: void onBack()
                  * 
                  *  Preconditions:
                  *    (soft) this.awayLabel != null
                  *    (soft) this.inputPanel != null
                  */
   455          setAwayIndicator(false);
   456      }
   457  
   458      /** {@inheritDoc} */
   459      @Override
   460      public void close() {
                 /* 
    P/P           *  Method: void close()
                  * 
                  *  Presumptions:
                  *    com.dmdirc.WritableFrameContainer:getServer(...)@464 != null
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:getContainer(...)@187 != null
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.WritableFrameContainer:getServer(...)@463: Addr_Set{null}, Inverse{null}
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:getContainer(...)@187: Addr_Set{null}, Inverse{null}
                  */
   461          super.close();
   462  
   463          if (getContainer() != null && getContainer().getServer() != null) {
   464              getContainer().getServer().removeAwayStateListener(this);
   465          }
   466      }
   467  }








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