File Source: TextFrame.java

             /* 
    P/P       *  Method: com.dmdirc.addons.ui_swing.components.frames.TextFrame$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.components.frames;
    24  
    25  import com.dmdirc.FrameContainer;
    26  import com.dmdirc.actions.ActionManager;
    27  import com.dmdirc.actions.CoreActionType;
    28  import com.dmdirc.addons.ui_swing.SwingController;
    29  import com.dmdirc.addons.ui_swing.UIUtilities;
    30  import com.dmdirc.addons.ui_swing.actions.ChannelCopyAction;
    31  import com.dmdirc.addons.ui_swing.actions.CommandAction;
    32  import com.dmdirc.addons.ui_swing.actions.HyperlinkCopyAction;
    33  import com.dmdirc.addons.ui_swing.actions.NicknameCopyAction;
    34  import com.dmdirc.addons.ui_swing.actions.SearchAction;
    35  import com.dmdirc.addons.ui_swing.actions.TextPaneCopyAction;
    36  import com.dmdirc.addons.ui_swing.components.LoggingSwingWorker;
    37  import com.dmdirc.addons.ui_swing.components.SwingSearchBar;
    38  import com.dmdirc.addons.ui_swing.textpane.ClickType;
    39  import com.dmdirc.addons.ui_swing.textpane.LineInfo;
    40  import com.dmdirc.addons.ui_swing.textpane.TextPane;
    41  import com.dmdirc.addons.ui_swing.textpane.TextPanePageDownAction;
    42  import com.dmdirc.addons.ui_swing.textpane.TextPanePageUpAction;
    43  import com.dmdirc.commandparser.PopupManager;
    44  import com.dmdirc.commandparser.PopupMenu;
    45  import com.dmdirc.commandparser.PopupMenuItem;
    46  import com.dmdirc.commandparser.PopupType;
    47  import com.dmdirc.commandparser.parsers.GlobalCommandParser;
    48  import com.dmdirc.util.StringTranscoder;
    49  import com.dmdirc.config.ConfigManager;
    50  import com.dmdirc.interfaces.ConfigChangeListener;
    51  import com.dmdirc.interfaces.IconChangeListener;
    52  import com.dmdirc.logger.ErrorLevel;
    53  import com.dmdirc.logger.Logger;
    54  import com.dmdirc.ui.WindowManager;
    55  import com.dmdirc.ui.interfaces.InputWindow;
    56  import com.dmdirc.ui.interfaces.Window;
    57  import com.dmdirc.ui.messages.Formatter;
    58  import com.dmdirc.util.URLHandler;
    59  
    60  import java.awt.Dimension;
    61  import java.awt.Point;
    62  import java.awt.event.KeyEvent;
    63  import java.awt.event.KeyListener;
    64  import java.awt.event.MouseEvent;
    65  import java.awt.event.MouseListener;
    66  import java.beans.PropertyChangeEvent;
    67  import java.beans.PropertyChangeListener;
    68  import java.beans.PropertyVetoException;
    69  import java.lang.reflect.Constructor;
    70  import java.lang.reflect.InvocationTargetException;
    71  import java.nio.charset.Charset;
    72  import java.nio.charset.IllegalCharsetNameException;
    73  import java.nio.charset.UnsupportedCharsetException;
    74  import java.util.Date;
    75  import java.util.LinkedList;
    76  import java.util.List;
    77  
    78  import java.util.concurrent.atomic.AtomicBoolean;
    79  import javax.swing.BorderFactory;
    80  import javax.swing.Icon;
    81  import javax.swing.JComponent;
    82  import javax.swing.JInternalFrame;
    83  import javax.swing.JMenu;
    84  import javax.swing.JMenuItem;
    85  import javax.swing.JPopupMenu;
    86  import javax.swing.JSeparator;
    87  import javax.swing.KeyStroke;
    88  import javax.swing.UIManager;
    89  import javax.swing.WindowConstants;
    90  import javax.swing.event.InternalFrameEvent;
    91  import javax.swing.event.InternalFrameListener;
    92  import javax.swing.plaf.basic.BasicInternalFrameUI;
    93  import javax.swing.plaf.synth.SynthLookAndFeel;
    94  
    95  /**
    96   * Implements a generic (internal) frame.
    97   */
         /* 
    P/P   *  Method: int access$900(TextFrame)
          * 
          *  Preconditions:
          *    x0 != null
          *    init'ed(x0.frameBufferSize)
          * 
          *  Postconditions:
          *    return_value == x0.frameBufferSize
          *    init'ed(return_value)
          */
    98  public abstract class TextFrame extends JInternalFrame implements Window,
    99          PropertyChangeListener, InternalFrameListener,
   100          MouseListener, KeyListener, ConfigChangeListener {
   101  
   102      /** Logger to use. */
             /* 
    P/P       *  Method: com.dmdirc.addons.ui_swing.components.frames.TextFrame__static_init
              * 
              *  Postconditions:
              *    init'ed(LOGGER)
              */
   103      private static final java.util.logging.Logger LOGGER =
   104              java.util.logging.Logger.getLogger(TextFrame.class.getName());
   105      /**
   106       * A version number for this class. It should be changed whenever the class
   107       * structure is changed (or anything else that would prevent serialized
   108       * objects being unserialized with the new class).
   109       */
   110      private static final long serialVersionUID = 5;
   111      /** The channel object that owns this frame. */
   112      protected final FrameContainer frameParent;
   113      /** Frame output pane. */
   114      private TextPane textPane;
   115      /** search bar. */
   116      private SwingSearchBar searchBar;
   117      /** String transcoder. */
   118      private StringTranscoder transcoder;
   119      /** Frame buffer size. */
   120      private int frameBufferSize;
   121      /** Quick copy? */
   122      private boolean quickCopy;
   123      /** Are we closing? */
   124      private boolean closing = false;
   125      /** Input window for popup commands. */
   126      private Window inputWindow;
   127      /** Swing controller. */
   128      private SwingController controller;
   129      /** Are we maximising/restoring? */
   130      private AtomicBoolean maximiseRestoreInProgress = new AtomicBoolean(false);
   131  
   132      /** Click types. */
             /* 
    P/P       *  Method: void com.dmdirc.addons.ui_swing.components.frames.TextFrame$MouseClickType(String, int)
              */
   133      public enum MouseClickType {
   134  
   135          /** Clicked. */
                 /* 
    P/P           *  Method: com.dmdirc.addons.ui_swing.components.frames.TextFrame$MouseClickType__static_init
                  * 
                  *  Postconditions:
                  *    $VALUES == &new TextFrame$MouseClickType[](TextFrame$MouseClickType__static_init#4)
                  *    CLICKED == &new TextFrame$MouseClickType(TextFrame$MouseClickType__static_init#1)
                  *    $VALUES[0] == &new TextFrame$MouseClickType(TextFrame$MouseClickType__static_init#1)
                  *    PRESSED == &new TextFrame$MouseClickType(TextFrame$MouseClickType__static_init#3)
                  *    $VALUES[2] == &new TextFrame$MouseClickType(TextFrame$MouseClickType__static_init#3)
                  *    RELEASED == &new TextFrame$MouseClickType(TextFrame$MouseClickType__static_init#2)
                  *    $VALUES[1] == &new TextFrame$MouseClickType(TextFrame$MouseClickType__static_init#2)
                  *    new TextFrame$MouseClickType(TextFrame$MouseClickType__static_init#1) num objects == 1
                  *    new TextFrame$MouseClickType(TextFrame$MouseClickType__static_init#2) num objects == 1
                  *    new TextFrame$MouseClickType(TextFrame$MouseClickType__static_init#3) num objects == 1
                  *    ...
                  */
   136          CLICKED,
   137          /** Released. */
   138          RELEASED,
   139          /** Pressed. */
   140          PRESSED,
   141      }
   142  
   143      /**
   144       * Creates a new instance of Frame.
   145       *
   146       * @param owner FrameContainer owning this frame.
   147       * @param controller Swing controller
   148       */
   149      public TextFrame(final FrameContainer owner,
   150              final SwingController controller) {
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.components.frames.TextFrame(FrameContainer, SwingController)
                  * 
                  *  Preconditions:
                  *    controller != null
                  *    owner != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.FrameContainer:getConfigManager(...)@155 != null
                  *    com.dmdirc.addons.ui_swing.SwingController:getMainFrame(...)@190 != null
                  * 
                  *  Postconditions:
                  *    init'ed(this.closing)
                  *    this.controller == controller
                  *    this.controller != null
                  *    init'ed(this.frameBufferSize)
                  *    this.frameParent == owner
                  *    this.frameParent != null
                  *    init'ed(this.inputWindow)
                  *    this.maximiseRestoreInProgress == &new AtomicBoolean(TextFrame#1)
                  *    init'ed(this.quickCopy)
                  *    this.searchBar == &new SwingSearchBar(initComponents#2)
                  *    ...
                  */
   151          super();
   152          this.controller = controller;
   153          frameParent = owner;
   154  
   155          final ConfigManager config = owner.getConfigManager();
   156          frameBufferSize = config.getOptionInt("ui", "frameBufferSize");
   157          quickCopy = config.getOptionBool("ui", "quickCopy");
   158          setFrameIcon(owner.getIcon());
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.components.frames.TextFrame$1(TextFrame)
                  */
   159          owner.addIconChangeListener(new IconChangeListener() {
   160  
   161              /** {@inheritDoc} */
   162              @Override
   163              public void iconChanged(final Window window, final Icon icon) {
                         /* 
    P/P                   *  Method: void iconChanged(Window, Icon)
                          */
   164                  setFrameIcon(icon);
   165              }
   166          });
   167  
   168          try {
   169              transcoder = new StringTranscoder(Charset.forName(
   170                      config.getOption("channel", "encoding")));
   171          } catch (UnsupportedCharsetException ex) {
   172              transcoder = new StringTranscoder(Charset.forName("UTF-8"));
   173          } catch (IllegalCharsetNameException ex) {
   174              transcoder = new StringTranscoder(Charset.forName("UTF-8"));
   175          } catch (IllegalArgumentException ex) {
   176              transcoder = new StringTranscoder(Charset.forName("UTF-8"));
   177          }
   178  
   179          inputWindow = this;
   180          while (!(inputWindow instanceof InputWindow) && inputWindow != null) {
   181              inputWindow = WindowManager.getParent(inputWindow);
   182          }
   183  
   184          initComponents();
   185          setMaximizable(true);
   186          setClosable(true);
   187          setResizable(true);
   188          setIconifiable(true);
   189          setFocusable(true);
   190          setPreferredSize(new Dimension(controller.getMainFrame().getWidth() /
   191                  2, controller.getMainFrame().getHeight() / 3));
   192          setDefaultCloseOperation(WindowConstants.DISPOSE_ON_CLOSE);
   193  
   194          addPropertyChangeListener("UI", this);
   195          addInternalFrameListener(this);
   196  
   197          getTextPane().setBackground(config.getOptionColour("ui",
   198                  "backgroundcolour"));
   199          getTextPane().setForeground(config.getOptionColour("ui",
   200                  "foregroundcolour"));
   201  
   202          config.addChangeListener("ui", "foregroundcolour", this);
   203          config.addChangeListener("ui", "backgroundcolour", this);
   204          config.addChangeListener("ui", "quickCopy", this);
   205          config.addChangeListener("ui", "frameBufferSize", this);
   206  
   207          addPropertyChangeListener("maximum", this);
   208      }
   209  
   210      /**
   211       * Returns this text frames swing controller.
   212       * 
   213       * @return Swing controller
   214       */
   215      public SwingController getController() {
                 /* 
    P/P           *  Method: SwingController getController()
                  * 
                  *  Preconditions:
                  *    init'ed(this.controller)
                  * 
                  *  Postconditions:
                  *    return_value == this.controller
                  *    init'ed(return_value)
                  */
   216          return controller;
   217      }
   218  
   219      /** {@inheritDoc} */
   220      @Override
   221      public void setTitle(final String title) {
                 /* 
    P/P           *  Method: void setTitle(String)
                  */
   222          UIUtilities.invokeLater(new Runnable() {
   223  
   224              /** {@inheritDoc} */
   225              @Override
   226              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          */
   227                  TextFrame.super.setTitle(title);
   228              }
   229          });
   230      }
   231  
   232      /** {@inheritDoc} */
   233      @Override
   234      public void setVisible(final boolean isVisible) {
                 /* 
    P/P           *  Method: void setVisible(bool)
                  */
   235          UIUtilities.invokeLater(new Runnable() {
   236  
   237              @Override
   238              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    (soft) this.frameParent != null
                          * 
                          *  Test Vectors:
                          *    this.val$isVisible: {0}, {1}
                          *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isVisible(...)@239: {0}, {1}
                          */
   239                  if (isVisible() && isVisible) {
   240                      open();
   241                  } else {
   242                      TextFrame.super.setVisible(isVisible);
   243                  }
   244              }
   245          });
   246      }
   247  
   248      /** {@inheritDoc} */
   249      @Override
   250      public void open() {
                 /* 
    P/P           *  Method: void open()
                  * 
                  *  Preconditions:
                  *    this.frameParent != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.FrameContainer:getConfigManager(...)@251 != null
                  */
   251          final boolean pref = frameParent.getConfigManager().getOptionBool("ui",
   252                      "maximisewindows");
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.components.frames.TextFrame$4(TextFrame, bool)
                  * 
                  *  Postconditions:
                  *    this.val$pref == Param_2
                  *    init'ed(this.val$pref)
                  */
   253          UIUtilities.invokeLater(new Runnable() {
   254  
   255              @Override
   256              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    (soft) this.controller != null
                          * 
                          *  Presumptions:
                          *    com.dmdirc.addons.ui_swing.SwingController:getMainFrame(...)@261 != null
                          * 
                          *  Test Vectors:
                          *    this.val$pref: {1}, {0}
                          *    com.dmdirc.addons.ui_swing.MainFrame:getMaximised(...)@261: {0}, {1}
                          *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isMaximum(...)@262: {1}, {0}
                          *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isSelected(...)@270: {1}, {0}
                          *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isVisible(...)@257: {1}, {0}
                          */
   257                  if (!isVisible()) {
   258                      TextFrame.super.setVisible(true);
   259                  }
   260                  try {
   261                      if (pref || controller.getMainFrame().getMaximised()) {
   262                          if (!isMaximum()) {
   263                              setMaximum(true);
   264                          }
   265                      }
   266                  } catch (PropertyVetoException ex) {
   267                      //Ignore
   268                  }
   269                  try {
   270                      if (!isSelected()) {
   271                          setSelected(true);
   272                      }
   273                  } catch (PropertyVetoException ex) {
   274                      //Ignore
   275                  }
   276              }
   277          });
   278      }
   279  
   280      /** {@inheritDoc} */
   281      @Override
   282      public void activateFrame() {
                 /* 
    P/P           *  Method: void activateFrame()
                  */
   283          UIUtilities.invokeLater(new Runnable() {
   284  
   285              @Override
   286              public void run() {
   287                  try {
                             /* 
    P/P                       *  Method: void run()
                              * 
                              *  Presumptions:
                              *    init'ed(com.dmdirc.actions.CoreActionType.CLIENT_FRAME_CHANGED)
                              * 
                              *  Test Vectors:
                              *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isIcon(...)@288: {0}, {1}
                              *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isSelected(...)@294: {1}, {0}
                              *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isVisible(...)@291: {1}, {0}
                              */
   288                      if (isIcon()) {
   289                          setIcon(false);
   290                      }
   291                      if (!isVisible()) {
   292                          TextFrame.super.setVisible(true);
   293                      }
   294                      if (!isSelected()) {
   295                          ActionManager.processEvent(
   296                              CoreActionType.CLIENT_FRAME_CHANGED,
   297                              null, getContainer());
   298                          setSelected(true);
   299                      }
   300                  } catch (PropertyVetoException ex) {
   301                      //Ignore
   302                  }
   303              }
   304          });
   305      }
   306  
   307      /** Closes this frame. */
   308      @Override
   309      public void close() {
                 /* 
    P/P           *  Method: void close()
                  */
   310          UIUtilities.invokeLater(new Runnable() {
   311  
   312              @Override
   313              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    init'ed(this.closing)
                          * 
                          *  Presumptions:
                          *    init'ed(com.dmdirc.logger.ErrorLevel.LOW)
                          * 
                          *  Test Vectors:
                          *    this.closing: {0}, {1}
                          *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isClosed(...)@321: {1}, {0}
                          */
   314                  if (closing) {
   315                      return;
   316                  }
   317  
   318                  closing = true;
   319  
   320                  try {
   321                      if (!isClosed()) {
   322                          setClosed(true);
   323                      }
   324                  } catch (PropertyVetoException ex) {
   325                      Logger.userError(ErrorLevel.LOW, "Unable to close frame");
   326                  }
   327  
   328              }
   329          });
   330      }
   331  
   332      /** {@inheritDoc} */
   333      @Override
   334      public void minimise() {
                 /* 
    P/P           *  Method: void minimise()
                  */
   335          UIUtilities.invokeLater(new Runnable() {
   336  
   337              @Override
   338              public void run() {
   339                  try {
                             /* 
    P/P                       *  Method: void run()
                              * 
                              *  Presumptions:
                              *    init'ed(com.dmdirc.logger.ErrorLevel.LOW)
                              * 
                              *  Test Vectors:
                              *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isIcon(...)@340: {1}, {0}
                              */
   340                      if (!isIcon()) {
   341                          setIcon(true);
   342                      }
   343                  } catch (PropertyVetoException ex) {
   344                      Logger.userError(ErrorLevel.LOW, "Unable to minimise frame");
   345                  }
   346              }
   347          });
   348      }
   349  
   350      /** {@inheritDoc} */
   351      @Override
   352      public void maximise() {
                 /* 
    P/P           *  Method: void maximise()
                  * 
                  *  Presumptions:
                  *    java.util.logging.Logger:getLogger(...)@103 != null
                  */
   353          LOGGER.finest("maximise(): About to invokeAndWait");
   354  
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.components.frames.TextFrame$8(TextFrame)
                  */
   355          UIUtilities.invokeLater(new Runnable() {
   356  
   357              /** {@inheritDoc} */
   358              @Override
   359              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    (soft) this.maximiseRestoreInProgress != null
                          * 
                          *  Presumptions:
                          *    init'ed(com.dmdirc.logger.ErrorLevel.LOW)
                          *    java.util.logging.Logger:getLogger(...)@103 != null
                          * 
                          *  Test Vectors:
                          *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isIcon(...)@369: {0}, {1}
                          *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isMaximum(...)@363: {0}, {1}
                          */
   360                  LOGGER.finest("maximise(): Running");
   361  
   362                  try {
   363                      if (isMaximum()) {
   364                          return;
   365                      }
   366  
   367                      maximiseRestoreInProgress.set(true);
   368                      LOGGER.finest("maximise(): About to set icon");
   369                      if (isIcon()) {
   370                          setIcon(false);
   371                      }
   372                      LOGGER.finest("maximise(): About to set maximum");
   373                      setMaximum(true);
   374                      LOGGER.finest("maximise(): Done?");
   375                  } catch (PropertyVetoException ex) {
   376                      Logger.userError(ErrorLevel.LOW, "Unable to minimise frame");
   377                  }
   378                  maximiseRestoreInProgress.set(false);
   379  
   380                  LOGGER.finest("maximise(): Done running");
   381              }
   382          });
   383          LOGGER.finest("maximise(): Done");
   384      }
   385  
   386      /** {@inheritDoc} */
   387      @Override
   388      public void restore() {
                 /* 
    P/P           *  Method: void restore()
                  */
   389          UIUtilities.invokeLater(new Runnable() {
   390  
   391              /** {@inheritDoc} */
   392              @Override
   393              public void run() {
   394                  try {
                             /* 
    P/P                       *  Method: void run()
                              * 
                              *  Preconditions:
                              *    (soft) this.maximiseRestoreInProgress != null
                              * 
                              *  Presumptions:
                              *    init'ed(com.dmdirc.logger.ErrorLevel.LOW)
                              * 
                              *  Test Vectors:
                              *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isIcon(...)@400: {0}, {1}
                              *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isMaximum(...)@395: {1}, {0}
                              */
   395                      if (!isMaximum()) {
   396                          return;
   397                      }
   398  
   399                      maximiseRestoreInProgress.set(true);
   400                      if (isIcon()) {
   401                          setIcon(false);
   402                      }
   403                      setMaximum(false);
   404                  } catch (PropertyVetoException ex) {
   405                      Logger.userError(ErrorLevel.LOW, "Unable to minimise frame");
   406                  }
   407                  maximiseRestoreInProgress.set(false);
   408              }
   409          });
   410      }
   411  
   412      /** {@inheritDoc} */
   413      @Override
   414      public void toggleMaximise() {
                 /* 
    P/P           *  Method: void toggleMaximise()
                  */
   415          UIUtilities.invokeLater(new Runnable() {
   416  
   417              /** {@inheritDoc} */
   418              @Override
   419              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Test Vectors:
                          *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isMaximum(...)@420: {0}, {1}
                          */
   420                  if (isMaximum()) {
   421                      restore();
   422                  } else {
   423                      maximise();
   424                  }
   425              }
   426          });
   427      }
   428  
   429      /** {@inheritDoc} */
   430      @Override
   431      public final void addLine(final String line, final boolean timestamp) {
                 /* 
    P/P           *  Method: void addLine(String, bool)
                  * 
                  *  Preconditions:
                  *    this.transcoder != null
                  */
   432          final String encodedLine = transcoder.decode(line);
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.components.frames.TextFrame$11(TextFrame, String, bool)
                  * 
                  *  Postconditions:
                  *    this.val$encodedLine == Param_2
                  *    init'ed(this.val$encodedLine)
                  *    this.val$timestamp == Param_3
                  *    init'ed(this.val$timestamp)
                  */
   433          UIUtilities.invokeLater(new Runnable() {
   434  
   435              /** {@inheritDoc} */
   436              @Override
   437              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    init'ed(this.frameBufferSize)
                          *    this.textPane != null
                          *    this.val$encodedLine != null
                          * 
                          *  Presumptions:
                          *    com.dmdirc.addons.ui_swing.textpane.TextPane:getDocument(...)@461 != null
                          * 
                          *  Test Vectors:
                          *    this.frameBufferSize: {-231..0}, {1..232-1}
                          */
   438                  final List<String[]> lines = new LinkedList<String[]>();
   439                  for (final String myLine : encodedLine.split("\n")) {
   440                      if (timestamp) {
   441                          lines.add(new String[]{
   442                                      Formatter.formatMessage(getConfigManager(),
   443                                      "timestamp", new Date()), myLine,});
   444                      } else {
   445                          lines.add(new String[]{myLine,});
   446                      }
   447  
                             /* 
    P/P                       *  Method: void com.dmdirc.addons.ui_swing.components.frames.TextFrame$11$1(TextFrame$11, String)
                              * 
                              *  Postconditions:
                              *    this.val$myLine == Param_2
                              *    init'ed(this.val$myLine)
                              */
   448                      new LoggingSwingWorker() {
   449  
   450                          /** {@inheritDoc} */
   451                          @Override
   452                          protected Object doInBackground() throws Exception {
                                     /* 
    P/P                               *  Method: Object doInBackground()
                                      * 
                                      *  Presumptions:
                                      *    init'ed(com.dmdirc.actions.CoreActionType.CLIENT_LINE_ADDED)
                                      * 
                                      *  Postconditions:
                                      *    return_value == null
                                      */
   453                              ActionManager.processEvent(
   454                                      CoreActionType.CLIENT_LINE_ADDED,
   455                                      null, getContainer(), myLine);
   456                              return null;
   457                          }
   458                      }.execute();
   459                  }
   460  
   461                  textPane.getDocument().addText(lines);
   462  
   463                  if (frameBufferSize > 0) {
   464                      textPane.trim(frameBufferSize);
   465                  }
   466              }
   467          });
   468      }
   469  
   470      /** {@inheritDoc} */
   471      @Override
   472      public final void addLine(final String messageType,
   473              final Object... args) {
                 /* 
    P/P           *  Method: void addLine(String, Object[])
                  * 
                  *  Preconditions:
                  *    messageType != null
                  *    (soft) this.frameParent != null
                  *    (soft) this.transcoder != null
                  * 
                  *  Test Vectors:
                  *    java.lang.String:isEmpty(...)@474: {1}, {0}
                  */
   474          if (!messageType.isEmpty()) {
   475              addLine(Formatter.formatMessage(getConfigManager(), messageType,
   476                      args), true);
   477          }
   478  
   479      }
   480  
   481      /** {@inheritDoc} */
   482      @Override
   483      public final void addLine(final StringBuffer messageType,
   484              final Object... args) {
                 /* 
    P/P           *  Method: void addLine(StringBuffer, Object[])
                  * 
                  *  Preconditions:
                  *    (soft) this.frameParent != null
                  *    (soft) this.transcoder != null
                  * 
                  *  Test Vectors:
                  *    messageType: Addr_Set{null}, Inverse{null}
                  */
   485          if (messageType != null) {
   486              addLine(messageType.toString(), args);
   487          }
   488  
   489      }
   490  
   491      /** {@inheritDoc} */
   492      @Override
   493      public final void clear() {
                 /* 
    P/P           *  Method: void clear()
                  */
   494          UIUtilities.invokeLater(new Runnable() {
   495  
   496              /** {@inheritDoc} */
   497              @Override
   498              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    this.textPane != null
                          */
   499                  getTextPane().clear();
   500              }
   501          });
   502      }
   503  
   504      /**
   505       * Initialises the components for this frame.
   506       */
   507      private void initComponents() {
                 /* 
    P/P           *  Method: void initComponents()
                  * 
                  *  Preconditions:
                  *    this.controller != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:getActionMap(...)@532 != null
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:getActionMap(...)@534 != null
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:getActionMap(...)@536 != null
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:getInputMap(...)@517 != null
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:getInputMap(...)@521 != null
                  *    ...
                  * 
                  *  Postconditions:
                  *    this.searchBar == &amp;new SwingSearchBar(initComponents#2)
                  *    this.textPane == &amp;new TextPane(initComponents#1)
                  *    new SwingSearchBar(initComponents#2) num objects == 1
                  *    new TextPane(initComponents#1) num objects == 1
                  */
   508          setTextPane(new TextPane(getContainer()));
   509  
   510          getTextPane().addMouseListener(this);
   511          getTextPane().addKeyListener(this);
   512  
   513          searchBar = new SwingSearchBar(this, controller.getMainFrame());
   514          searchBar.setVisible(false);
   515          searchBar.addKeyListener(this);
   516  
   517          getInputMap(JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT).
   518                  put(KeyStroke.getKeyStroke(KeyEvent.VK_PAGE_UP, 0),
   519                  "pageUpAction");
   520  
   521          getInputMap(JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT).
   522                  put(KeyStroke.getKeyStroke(KeyEvent.VK_PAGE_DOWN, 0),
   523                  "pageDownAction");
   524  
   525          getInputMap(JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT).
   526                  put(KeyStroke.getKeyStroke(KeyEvent.VK_F3, 0), "searchAction");
   527  
   528          getInputMap(JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT).
   529                  put(KeyStroke.getKeyStroke(KeyEvent.VK_F,
   530                  UIUtilities.getCtrlDownMask()), "searchAction");
   531  
   532          getActionMap().put("pageUpAction",
   533                  new TextPanePageUpAction(getTextPane()));
   534          getActionMap().put("pageDownAction",
   535                  new TextPanePageDownAction(getTextPane()));
   536          getActionMap().put("searchAction", new SearchAction(searchBar));
   537      }
   538  
   539      /**
   540       * Removes and reinserts the border of an internal frame on maximising.
   541       * {@inheritDoc}
   542       * 
   543       * @param event Property change event
   544       */
   545      @Override
   546      public final void propertyChange(final PropertyChangeEvent event) {
                 /* 
    P/P           *  Method: void propertyChange(PropertyChangeEvent)
                  * 
                  *  Preconditions:
                  *    event != null
                  * 
                  *  Presumptions:
                  *    java.beans.PropertyChangeEvent:getNewValue(...)@554 != null
                  *    java.util.logging.Logger:getLogger(...)@103 != null
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:isMaximum(...)@550: {0}, {1}
                  *    java.lang.Boolean:booleanValue(...)@554: {0}, {1}
                  *    java.lang.String:equals(...)@549: {0}, {1}
                  */
   547          LOGGER.finer("Property change: name: " + event.getPropertyName() +
   548                  " value: " + event.getOldValue() + "->" + event.getNewValue());
   549          if ("UI".equals(event.getPropertyName())) {
   550              if (isMaximum()) {
   551                  hideTitlebar();
   552              }
   553          } else {
   554              if ((Boolean) event.getNewValue()) {
   555                  hideTitlebar();
   556              } else {
   557                  showTitlebar();
   558              }
   559          }
   560          LOGGER.finest("Done property change");
   561      }
   562  
   563      /** Hides the titlebar for this frame. */
   564      private void hideTitlebar() {
                 /* 
    P/P           *  Method: void hideTitlebar()
                  */
   565          UIUtilities.invokeLater(new Runnable() {
   566  
   567              /** {@inheritDoc} */
   568              @Override
   569              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Presumptions:
                          *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:getUI(...)@571 != null
                          */
   570                  setBorder(BorderFactory.createEmptyBorder(0, 0, 0, 0));
   571                  ((BasicInternalFrameUI) getUI()).setNorthPane(null);
   572              }
   573          });
   574      }
   575  
   576      /** Shows the titlebar for this frame. */
   577      private void showTitlebar() {
                 /* 
    P/P           *  Method: void showTitlebar()
                  */
   578          UIUtilities.invokeLater(new Runnable() {
   579  
   580              /** {@inheritDoc} */
   581              @Override
   582              public void run() {
   583                  final Class<?> c;
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Presumptions:
                          *    init'ed(com.dmdirc.logger.ErrorLevel.MEDIUM)
                          *    java.lang.Class:getClassLoader(...)@594 != null
                          *    java.lang.Class:getConstructor(...)@595 != null
                          *    java.lang.ClassLoader:loadClass(...)@594 != null
                          *    java.lang.Object:getClass(...)@594 != null
                          * 
                          *  Test Vectors:
                          *    java.lang.String:equals(...)@590: {0}, {1}
                          */
   584                  Object temp = null;
   585                  Constructor<?> constructor;
   586  
   587                  final String componentUI = (String) UIManager.get(
   588                          "InternalFrameUI");
   589  
   590                  if ("javax.swing.plaf.synth.SynthLookAndFeel".equals(componentUI)) {
   591                      temp = SynthLookAndFeel.createUI(TextFrame.this);
   592                  } else {
   593                      try {
   594                          c = getClass().getClassLoader().loadClass(componentUI);
   595                          constructor =
   596                                  c.getConstructor(new Class[]{
   597                                      javax.swing.JInternalFrame.class});
   598                          temp =
   599                                  constructor.newInstance(new Object[]{
   600                                      TextFrame.this});
   601                      } catch (ClassNotFoundException ex) {
   602                          Logger.appError(ErrorLevel.MEDIUM,
   603                                  "Unable to readd titlebar",
   604                                  ex);
   605                      } catch (NoSuchMethodException ex) {
   606                          Logger.appError(ErrorLevel.MEDIUM,
   607                                  "Unable to readd titlebar",
   608                                  ex);
   609                      } catch (InstantiationException ex) {
   610                          Logger.appError(ErrorLevel.MEDIUM,
   611                                  "Unable to readd titlebar",
   612                                  ex);
   613                      } catch (IllegalAccessException ex) {
   614                          Logger.appError(ErrorLevel.MEDIUM,
   615                                  "Unable to readd titlebar",
   616                                  ex);
   617                      } catch (InvocationTargetException ex) {
   618                          Logger.appError(ErrorLevel.MEDIUM,
   619                                  "Unable to readd titlebar",
   620                                  ex);
   621                      }
   622  
   623                  }
   624  
   625                  setBorder(UIManager.getBorder("InternalFrame.border"));
   626                  if (temp == null) {
   627                      temp = new BasicInternalFrameUI(TextFrame.this);
   628                  }
   629  
   630                  setUI((BasicInternalFrameUI) temp);
   631              }
   632          });
   633      }
   634  
   635      /**
   636       * Not needed for this class. {@inheritDoc}
   637       * 
   638       * @param event Internal frame event
   639       */
   640      @Override
   641      public void internalFrameOpened(final InternalFrameEvent event) {
                 /* 
    P/P           *  Method: void internalFrameOpened(InternalFrameEvent)
                  */
   642          new LoggingSwingWorker() {
   643  
   644              /** {@inheritDoc} */
   645              @Override
   646              protected Object doInBackground() throws Exception {
                         /* 
    P/P                   *  Method: Object doInBackground()
                          * 
                          *  Preconditions:
                          *    this.frameParent != null
                          * 
                          *  Postconditions:
                          *    return_value == null
                          */
   647                  frameParent.windowOpened();
   648                  return null;
   649              }
   650          }.execute();
   651      }
   652  
   653      /**
   654       * Not needed for this class. {@inheritDoc}
   655       * 
   656       * @param event Internal frame event
   657       */
   658      @Override
   659      public void internalFrameClosing(final InternalFrameEvent event) {
                 /* 
    P/P           *  Method: void internalFrameClosing(InternalFrameEvent)
                  */
   660          new LoggingSwingWorker() {
   661  
   662              /** {@inheritDoc} */
   663              @Override
   664              protected Object doInBackground() throws Exception {
                         /* 
    P/P                   *  Method: Object doInBackground()
                          * 
                          *  Preconditions:
                          *    this.frameParent != null
                          * 
                          *  Postconditions:
                          *    return_value == null
                          */
   665                  frameParent.windowClosing();
   666                  return null;
   667              }
   668          }.execute();
   669      }
   670  
   671      /**
   672       * Not needed for this class. {@inheritDoc}
   673       * 
   674       * @param event Internal frame event
   675       */
   676      @Override
   677      public void internalFrameClosed(final InternalFrameEvent event) {
                 /* 
    P/P           *  Method: void internalFrameClosed(InternalFrameEvent)
                  */
   678          new LoggingSwingWorker() {
   679  
   680              /** {@inheritDoc} */
   681              @Override
   682              protected Object doInBackground() throws Exception {
                         /* 
    P/P                   *  Method: Object doInBackground()
                          * 
                          *  Preconditions:
                          *    this.frameParent != null
                          * 
                          *  Postconditions:
                          *    return_value == null
                          */
   683                  frameParent.windowClosed();
   684                  return null;
   685              }
   686          }.execute();
   687      }
   688  
   689      /**
   690       * Makes the internal frame invisible. {@inheritDoc}
   691       * 
   692       * @param event Internal frame event
   693       */
   694      @Override
   695      public void internalFrameIconified(final InternalFrameEvent event) {
                 /* 
    P/P           *  Method: void internalFrameIconified(InternalFrameEvent)
                  */
   696          UIUtilities.invokeLater(new Runnable() {
   697  
   698              @Override
   699              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          * 
                          *  Preconditions:
                          *    this.val$event != null
                          * 
                          *  Presumptions:
                          *    javax.swing.event.InternalFrameEvent:getInternalFrame(...)@700 != null
                          */
   700                  event.getInternalFrame().setVisible(false);
   701              }
   702          });
   703      }
   704  
   705      /**
   706       * Not needed for this class. {@inheritDoc}
   707       * 
   708       * @param event Internal frame event
   709       */
   710      @Override
   711      public void internalFrameDeiconified(final InternalFrameEvent event) {
   712          //Ignore.
                 /* 
    P/P           *  Method: void internalFrameDeiconified(InternalFrameEvent)
                  */
   713          }
   714  
   715      /**
   716       * Activates the input field on frame focus. {@inheritDoc}
   717       * 
   718       * @param event Internal frame event
   719       */
   720      @Override
   721      public void internalFrameActivated(final InternalFrameEvent event) {
                 /* 
    P/P           *  Method: void internalFrameActivated(InternalFrameEvent)
                  * 
                  *  Preconditions:
                  *    this.maximiseRestoreInProgress != null
                  * 
                  *  Presumptions:
                  *    java.util.logging.Logger:getLogger(...)@103 != null
                  * 
                  *  Test Vectors:
                  *    java.util.concurrent.atomic.AtomicBoolean:get(...)@724: {0}, {1}
                  */
   722          LOGGER.finer(getName() + ": internalFrameActivated()");
   723  
   724          if (maximiseRestoreInProgress.get()) {
   725              return;
   726          }
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.components.frames.TextFrame$19(TextFrame)
                  */
   727          new LoggingSwingWorker() {
   728  
   729              /** {@inheritDoc} */
   730              @Override
   731              protected Object doInBackground() throws Exception {
                         /* 
    P/P                   *  Method: Object doInBackground()
                          * 
                          *  Preconditions:
                          *    this.frameParent != null
                          * 
                          *  Presumptions:
                          *    java.util.logging.Logger:getLogger(...)@103 != null
                          * 
                          *  Postconditions:
                          *    return_value == null
                          */
   732                  LOGGER.finer(getName() +
   733                          ": internalFrameActivated(): doInBackground");
   734                  frameParent.windowActivated();
   735                  return null;
   736              }
   737          }.execute();
   738      }
   739  
   740      /**
   741       * Not needed for this class. {@inheritDoc}
   742       * 
   743       * @param event Internal frame event
   744       */
   745      @Override
   746      public void internalFrameDeactivated(final InternalFrameEvent event) {
                 /* 
    P/P           *  Method: void internalFrameDeactivated(InternalFrameEvent)
                  * 
                  *  Preconditions:
                  *    this.maximiseRestoreInProgress != null
                  * 
                  *  Test Vectors:
                  *    java.util.concurrent.atomic.AtomicBoolean:get(...)@747: {0}, {1}
                  */
   747          if (maximiseRestoreInProgress.get()) {
   748              return;
   749          }
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.components.frames.TextFrame$20(TextFrame)
                  */
   750          new LoggingSwingWorker() {
   751  
   752              /** {@inheritDoc} */
   753              @Override
   754              protected Object doInBackground() throws Exception {
                         /* 
    P/P                   *  Method: Object doInBackground()
                          * 
                          *  Preconditions:
                          *    this.frameParent != null
                          * 
                          *  Postconditions:
                          *    return_value == null
                          */
   755                  frameParent.windowDeactivated();
   756                  return null;
   757              }
   758          }.execute();
   759      }
   760  
   761      /** {@inheritDoc} */
   762      @Override
   763      public FrameContainer getContainer() {
                 /* 
    P/P           *  Method: FrameContainer getContainer()
                  * 
                  *  Postconditions:
                  *    return_value == this.frameParent
                  *    init'ed(return_value)
                  */
   764          return frameParent;
   765      }
   766  
   767      /** {@inheritDoc} */
   768      @Override
   769      public ConfigManager getConfigManager() {
                 /* 
    P/P           *  Method: ConfigManager getConfigManager()
                  * 
                  *  Preconditions:
                  *    this.frameParent != null
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   770          return getContainer().getConfigManager();
   771      }
   772  
   773      /**
   774       * Returns the text pane for this frame.
   775       *
   776       * @return Text pane for this frame
   777       */
   778      public final TextPane getTextPane() {
                 /* 
    P/P           *  Method: TextPane getTextPane()
                  * 
                  *  Preconditions:
                  *    init'ed(this.textPane)
                  * 
                  *  Postconditions:
                  *    return_value == this.textPane
                  *    init'ed(return_value)
                  */
   779          return textPane;
   780      }
   781  
   782      /**
   783       * Returns the transcoder for this frame.
   784       *
   785       * @return String transcoder for this frame
   786       */
   787      @Override
   788      public StringTranscoder getTranscoder() {
                 /* 
    P/P           *  Method: StringTranscoder getTranscoder()
                  * 
                  *  Preconditions:
                  *    init'ed(this.transcoder)
                  * 
                  *  Postconditions:
                  *    return_value == this.transcoder
                  *    init'ed(return_value)
                  */
   789          return transcoder;
   790      }
   791  
   792      /** {@inheritDoc} */
   793      @Override
   794      public final String getName() {
                 /* 
    P/P           *  Method: String getName()
                  * 
                  *  Postconditions:
                  *    init'ed(com.dmdirc.FrameContainer:toString(...)._tainted)
                  *    return_value in Addr_Set{&amp;com.dmdirc.FrameContainer:toString(...),&amp;""}
                  * 
                  *  Test Vectors:
                  *    this.frameParent: Inverse{null}, Addr_Set{null}
                  */
   795          if (frameParent == null) {
   796              return "";
   797          }
   798  
   799          return frameParent.toString();
   800      }
   801  
   802      /**
   803       * Sets the frames text pane.
   804       *
   805       * @param newTextPane new text pane to use
   806       */
   807      protected final void setTextPane(final TextPane newTextPane) {
                 /* 
    P/P           *  Method: void setTextPane(TextPane)
                  * 
                  *  Postconditions:
                  *    this.textPane == newTextPane
                  *    init'ed(this.textPane)
                  */
   808          this.textPane = newTextPane;
   809      }
   810  
   811      /**
   812       * {@inheritDoc}
   813       * 
   814       * @param mouseEvent Mouse event
   815       */
   816      @Override
   817      public void mouseClicked(final MouseEvent mouseEvent) {
                 /* 
    P/P           *  Method: void mouseClicked(MouseEvent)
                  * 
                  *  Preconditions:
                  *    mouseEvent != null
                  *    (soft) init'ed(com.dmdirc.addons.ui_swing.components.frames.TextFrame$21__static_init.new int[](TextFrame$21__static_init#1)[...])
                  *    (soft) this.frameParent != null
                  *    (soft) init'ed(this.inputWindow)
                  *    (soft) this.textPane != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.addons.ui_swing.textpane.ClickType:values(...).length >= 1
                  */
   818          if (mouseEvent.getSource() == getTextPane()) {
   819              processMouseClickEvent(mouseEvent, MouseClickType.CLICKED);
   820          }
   821  
   822      }
   823  
   824      /**
   825       * {@inheritDoc}
   826       * 
   827       * @param mouseEvent Mouse event
   828       */
   829      @Override
   830      public void mousePressed(final MouseEvent mouseEvent) {
                 /* 
    P/P           *  Method: void mousePressed(MouseEvent)
                  * 
                  *  Preconditions:
                  *    mouseEvent != null
                  *    this.textPane != null
                  *    (soft) init'ed(com.dmdirc.addons.ui_swing.components.frames.TextFrame$21__static_init.new int[](TextFrame$21__static_init#1)[...])
                  *    (soft) this.frameParent != null
                  *    (soft) init'ed(this.inputWindow)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.addons.ui_swing.textpane.ClickType:values(...).length >= 1
                  */
   831          processMouseClickEvent(mouseEvent, MouseClickType.PRESSED);
   832      }
   833  
   834      /**
   835       * {@inheritDoc}
   836       * 
   837       * @param mouseEvent Mouse event
   838       */
   839      @Override
   840      public void mouseReleased(final MouseEvent mouseEvent) {
                 /* 
    P/P           *  Method: void mouseReleased(MouseEvent)
                  * 
                  *  Preconditions:
                  *    init'ed(this.quickCopy)
                  *    (soft) init'ed(com.dmdirc.addons.ui_swing.components.frames.TextFrame$21__static_init.new int[](TextFrame$21__static_init#1)[...])
                  *    (soft) mouseEvent != null
                  *    (soft) this.frameParent != null
                  *    (soft) init'ed(this.inputWindow)
                  *    (soft) this.textPane != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.addons.ui_swing.textpane.ClickType:values(...).length >= 1
                  * 
                  *  Test Vectors:
                  *    this.quickCopy: {0}, {1}
                  */
   841          if (quickCopy && mouseEvent.getSource() == getTextPane()) {
   842              getTextPane().copy();
   843              getTextPane().clearSelection();
   844          }
   845  
   846          processMouseClickEvent(mouseEvent, MouseClickType.RELEASED);
   847      }
   848  
   849      /**
   850       * {@inheritDoc}
   851       * 
   852       * @param mouseEvent Mouse event
   853       */
   854      @Override
   855      public void mouseEntered(final MouseEvent mouseEvent) {
   856          //Ignore.
                 /* 
    P/P           *  Method: void mouseEntered(MouseEvent)
                  */
   857          }
   858  
   859      /**
   860       * {@inheritDoc}
   861       * 
   862       * @param mouseEvent Mouse event
   863       */
   864      @Override
   865      public void mouseExited(final MouseEvent mouseEvent) {
   866          //Ignore.
                 /* 
    P/P           *  Method: void mouseExited(MouseEvent)
                  */
   867          }
   868  
   869      /**
   870       * Processes every mouse button event to check for a popup trigger.
   871       *
   872       * @param e mouse event
   873       * @param type 
   874       */
   875      public void processMouseClickEvent(final MouseEvent e,
   876              final MouseClickType type) {
                 /* 
    P/P           *  Method: void processMouseClickEvent(MouseEvent, TextFrame$MouseClickType)
                  * 
                  *  Preconditions:
                  *    e != null
                  *    this.textPane != null
                  *    (soft) init'ed(com.dmdirc.addons.ui_swing.components.frames.TextFrame$21__static_init.new int[](TextFrame$21__static_init#1)[...])
                  *    (soft) this.frameParent != null
                  *    (soft) init'ed(this.inputWindow)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.FrameContainer:getServer(...)@889 != null
                  *    com.dmdirc.FrameContainer:getServer(...)@895 != null
                  *    com.dmdirc.FrameContainer:getServer(...)@896 != null
                  *    com.dmdirc.FrameContainer:getServer(...)@899 != null
                  *    com.dmdirc.FrameContainer:getServer(...)@900 != null
                  *    ...
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame$21__static_init.new int[](TextFrame$21__static_init#1)[...]: {1}, {2}, {3}, {-231..0, 4..232-1}
                  *    com.dmdirc.Server:hasQuery(...)@895: {0}, {1}
                  *    com.dmdirc.addons.ui_swing.textpane.TextPane:getMousePosition(...)@877: Addr_Set{null}, Inverse{null}
                  *    java.awt.event.MouseEvent:isPopupTrigger(...)@883: {0}, {1}
                  */
   877          final Point point = getTextPane().getMousePosition();
   878          if (e.getSource() == getTextPane() && point != null) {
   879              final LineInfo lineInfo = getTextPane().getClickPosition(point);
   880              final ClickType clickType = getTextPane().getClickType(lineInfo);
   881              final String attribute = (String) getTextPane().
   882                      getAttributeValueAtPoint(lineInfo);
   883              if (e.isPopupTrigger()) {
   884                  showPopupMenuInternal(clickType, point, attribute);
   885              } else {
   886                  if (type == MouseClickType.CLICKED) {
                             /* 
    P/P                       *  Method: com.dmdirc.addons.ui_swing.components.frames.TextFrame$21__static_init
                              * 
                              *  Presumptions:
                              *    com.dmdirc.addons.ui_swing.textpane.ClickType.CHANNEL != null
                              *    com.dmdirc.addons.ui_swing.textpane.ClickType.HYPERLINK != null
                              *    com.dmdirc.addons.ui_swing.textpane.ClickType.NICKNAME != null
                              *    com.dmdirc.addons.ui_swing.textpane.ClickType:ordinal(...)@887 >= 0
                              *    com.dmdirc.addons.ui_swing.textpane.ClickType:ordinal(...)@887 < com.dmdirc.addons.ui_swing.textpane.ClickType:values(...).length@887
                              *    ...
                              * 
                              *  Postconditions:
                              *    new int[](TextFrame$21__static_init#1) num objects == 1
                              */
   887                      switch (clickType) {
   888                          case CHANNEL:
   889                              frameParent.getServer().join(attribute);
   890                              break;
   891                          case HYPERLINK:
   892                              URLHandler.getURLHander().launchApp(attribute);
   893                              break;
   894                          case NICKNAME:
   895                              if (getContainer().getServer().hasQuery(attribute)) {
   896                                  getContainer().getServer().getQuery(attribute).
   897                                          activateFrame();
   898                              } else {
   899                                  getContainer().getServer().addQuery(attribute);
   900                                  getContainer().getServer().getQuery(attribute).
   901                                          show();
   902                              }
   903  
   904                              break;
   905                          default:
   906                              break;
   907                      }
   908  
   909                  }
   910              }
   911          }
   912          super.processMouseEvent(e);
   913      }
   914  
   915      /**
   916       * What popup type should be used for popup menus for nicknames
   917       * 
   918       * @return Appropriate popuptype for this frame
   919       */
   920      public abstract PopupType getNicknamePopupType();
   921  
   922      /**
   923       * What popup type should be used for popup menus for channels
   924       * 
   925       * @return Appropriate popuptype for this frame
   926       */
   927      public abstract PopupType getChannelPopupType();
   928  
   929      /**
   930       * What popup type should be used for popup menus for hyperlinks
   931       * 
   932       * @return Appropriate popuptype for this frame
   933       */
   934      public abstract PopupType getHyperlinkPopupType();
   935  
   936      /**
   937       * What popup type should be used for popup menus for normal clicks
   938       * 
   939       * @return Appropriate popuptype for this frame
   940       */
   941      public abstract PopupType getNormalPopupType();
   942  
   943      /**
   944       * A method called to add custom popup items.
   945       * 
   946       * @param popupMenu Popup menu to add popup items to
   947       */
   948      public abstract void addCustomPopupItems(final JPopupMenu popupMenu);
   949  
   950      /**
   951       * Shows a popup menu at the specified point for the specified click type
   952       * 
   953       * @param type ClickType Click type
   954       * @param point Point Point of the click
   955       * @param argument Word under the click
   956       */
   957      private void showPopupMenuInternal(final ClickType type,
   958              final Point point,
   959              final String argument) {
   960          final JPopupMenu popupMenu;
   961  
                 /* 
    P/P           *  Method: void showPopupMenuInternal(ClickType, Point, String)
                  * 
                  *  Preconditions:
                  *    point != null
                  *    init'ed(this.textPane)
                  *    type != null
                  *    (soft) init'ed(com.dmdirc.addons.ui_swing.components.frames.TextFrame$21__static_init.new int[](TextFrame$21__static_init#1)[...])
                  *    (soft) this.frameParent != null
                  *    (soft) init'ed(this.inputWindow)
                  * 
                  *  Presumptions:
                  *    (int) (java.awt.Point:getX(...)@996) in {-231..232-1}
                  *    (int) (java.awt.Point:getY(...)@996) in {-231..232-1}
                  *    com.dmdirc.addons.ui_swing.textpane.ClickType:ordinal(...)@962 >= 0
                  *    com.dmdirc.addons.ui_swing.textpane.ClickType:values(...).length >= 1
                  *    com.dmdirc.addons.ui_swing.textpane.ClickType:ordinal(...)@962 < com.dmdirc.addons.ui_swing.textpane.ClickType:values(...).length
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame$21__static_init.new int[](TextFrame$21__static_init#1)[...]: {1}, {2}, {3}, {-231..0, 4..232-1}
                  *    javax.swing.JPopupMenu:getComponentCount(...)@966: {-231..1}, {2..232-1}
                  *    javax.swing.JPopupMenu:getComponentCount(...)@974: {-231..1}, {2..232-1}
                  *    javax.swing.JPopupMenu:getComponentCount(...)@981: {-231..0}, {1..232-1}
                  */
   962          switch (type) {
   963              case CHANNEL:
   964                  popupMenu = getPopupMenu(getChannelPopupType(), argument);
   965                  popupMenu.add(new ChannelCopyAction(argument));
   966                  if (popupMenu.getComponentCount() > 1) {
   967                      popupMenu.addSeparator();
   968                  }
   969  
   970                  break;
   971              case HYPERLINK:
   972                  popupMenu = getPopupMenu(getHyperlinkPopupType(), argument);
   973                  popupMenu.add(new HyperlinkCopyAction(argument));
   974                  if (popupMenu.getComponentCount() > 1) {
   975                      popupMenu.addSeparator();
   976                  }
   977  
   978                  break;
   979              case NICKNAME:
   980                  popupMenu = getPopupMenu(getNicknamePopupType(), argument);
   981                  if (popupMenu.getComponentCount() > 0) {
   982                      popupMenu.addSeparator();
   983                  }
   984  
   985                  popupMenu.add(new NicknameCopyAction(argument));
   986                  break;
   987              default:
   988                  popupMenu = getPopupMenu(null, argument);
   989                  break;
   990          }
   991  
   992          popupMenu.add(new TextPaneCopyAction(getTextPane()));
   993  
   994          addCustomPopupItems(popupMenu);
   995  
   996          popupMenu.show(this, (int) point.getX(), (int) point.getY());
   997      }
   998  
   999      /**
  1000       * Shows a popup menu at the specified point for the specified click type
  1001       * 
  1002       * @param type ClickType Click type
  1003       * @param point Point Point of the click
  1004       * @param argument Word under the click
  1005       */
  1006      public void showPopupMenu(final ClickType type,
  1007              final Point point,
  1008              final String argument) {
  1009          final JPopupMenu popupMenu;
  1010  
                 /* 
    P/P           *  Method: void showPopupMenu(ClickType, Point, String)
                  * 
                  *  Preconditions:
                  *    point != null
                  *    type != null
                  *    (soft) init'ed(com.dmdirc.addons.ui_swing.components.frames.TextFrame$21__static_init.new int[](TextFrame$21__static_init#1)[...])
                  *    (soft) this.frameParent != null
                  *    (soft) init'ed(this.inputWindow)
                  * 
                  *  Presumptions:
                  *    (int) (java.awt.Point:getX(...)@1041) in {-231..232-1}
                  *    (int) (java.awt.Point:getY(...)@1041) in {-231..232-1}
                  *    com.dmdirc.addons.ui_swing.textpane.ClickType:ordinal(...)@1011 >= 0
                  *    com.dmdirc.addons.ui_swing.textpane.ClickType:values(...).length >= 1
                  *    com.dmdirc.addons.ui_swing.textpane.ClickType:ordinal(...)@1011 < com.dmdirc.addons.ui_swing.textpane.ClickType:values(...).length
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame$21__static_init.new int[](TextFrame$21__static_init#1)[...]: {1}, {2}, {3}, {-231..0, 4..232-1}
                  *    javax.swing.JPopupMenu:getComponentCount(...)@1015: {-231..1}, {2..232-1}
                  *    javax.swing.JPopupMenu:getComponentCount(...)@1023: {-231..1}, {2..232-1}
                  *    javax.swing.JPopupMenu:getComponentCount(...)@1030: {-231..0}, {1..232-1}
                  */
  1011          switch (type) {
  1012              case CHANNEL:
  1013                  popupMenu = getPopupMenu(getChannelPopupType(), argument);
  1014                  popupMenu.add(new ChannelCopyAction(argument));
  1015                  if (popupMenu.getComponentCount() > 1) {
  1016                      popupMenu.addSeparator();
  1017                  }
  1018  
  1019                  break;
  1020              case HYPERLINK:
  1021                  popupMenu = getPopupMenu(getHyperlinkPopupType(), argument);
  1022                  popupMenu.add(new HyperlinkCopyAction(argument));
  1023                  if (popupMenu.getComponentCount() > 1) {
  1024                      popupMenu.addSeparator();
  1025                  }
  1026  
  1027                  break;
  1028              case NICKNAME:
  1029                  popupMenu = getPopupMenu(getNicknamePopupType(), argument);
  1030                  if (popupMenu.getComponentCount() > 0) {
  1031                      popupMenu.addSeparator();
  1032                  }
  1033  
  1034                  popupMenu.add(new NicknameCopyAction(argument));
  1035                  break;
  1036              default:
  1037                  popupMenu = getPopupMenu(null, argument);
  1038                  break;
  1039          }
  1040  
  1041          popupMenu.show(this, (int) point.getX(), (int) point.getY());
  1042      }
  1043  
  1044      /**
  1045       * Builds a popup menu of a specified type
  1046       * 
  1047       * @param type type of menu to build
  1048       * @param arguments Arguments for the command
  1049       * 
  1050       * @return PopupMenu
  1051       */
  1052      public JPopupMenu getPopupMenu(
  1053              final PopupType type,
  1054              final Object... arguments) {
                 /* 
    P/P           *  Method: JPopupMenu getPopupMenu(PopupType, Object[])
                  * 
                  *  Preconditions:
                  *    (soft) this.frameParent != null
                  *    (soft) init'ed(this.inputWindow)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.commandparser.PopupManager:getMenu(...)@1058 != null
                  * 
                  *  Postconditions:
                  *    return_value == &amp;new JPopupMenu(getPopupMenu#1)
                  *    new JPopupMenu(getPopupMenu#1) num objects == 1
                  * 
                  *  Test Vectors:
                  *    type: Addr_Set{null}, Inverse{null}
                  */
  1055          JPopupMenu popupMenu = new JPopupMenu();
  1056  
  1057          if (type != null) {
  1058              popupMenu = (JPopupMenu) populatePopupMenu(popupMenu,
  1059                      PopupManager.getMenu(type, getConfigManager()),
  1060                      arguments);
  1061          }
  1062  
  1063          return popupMenu;
  1064      }
  1065  
  1066      /**
  1067       * Populates the specified popupmenu
  1068       * 
  1069       * @param menu Menu component
  1070       * @param popup Popup to get info from
  1071       * @param arguments Arguments for the command
  1072       * 
  1073       * @return Populated popup
  1074       */
  1075      private JComponent populatePopupMenu(final JComponent menu,
  1076              final PopupMenu popup,
  1077              final Object... arguments) {
                 /* 
    P/P           *  Method: JComponent populatePopupMenu(JComponent, PopupMenu, Object[])
                  * 
                  *  Preconditions:
                  *    popup != null
                  *    (soft) menu != null
                  *    (soft) init'ed(this.inputWindow)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.commandparser.PopupMenu:getItems(...)@1078 != null
                  *    com.dmdirc.commandparser.PopupMenuItem:getSubMenu(...)@1082 != null
                  *    java.util.Iterator:next(...)@1078 != null
                  * 
                  *  Postconditions:
                  *    return_value == menu
                  *    return_value != null
                  * 
                  *  Test Vectors:
                  *    this.inputWindow: Inverse{null}, Addr_Set{null}
                  *    com.dmdirc.commandparser.PopupMenuItem:isDivider(...)@1079: {0}, {1}
                  *    com.dmdirc.commandparser.PopupMenuItem:isSubMenu(...)@1081: {0}, {1}
                  *    java.util.Iterator:hasNext(...)@1078: {0}, {1}
                  */
  1078          for (PopupMenuItem menuItem : popup.getItems()) {
  1079              if (menuItem.isDivider()) {
  1080                  menu.add(new JSeparator());
  1081              } else if (menuItem.isSubMenu()) {
  1082                  menu.add(populatePopupMenu(new JMenu(menuItem.getName()),
  1083                          menuItem.getSubMenu(), arguments));
  1084              } else {
  1085                  menu.add(new JMenuItem(new CommandAction(inputWindow == null ? GlobalCommandParser.
  1086                          getGlobalCommandParser()
  1087                          : ((InputWindow) inputWindow).getCommandParser(),
  1088                          (InputWindow) inputWindow, menuItem.getName(),
  1089                          menuItem.getCommand(arguments))));
  1090              }
  1091  
  1092          }
  1093          return menu;
  1094      }
  1095  
  1096      /** 
  1097       * {@inheritDoc}
  1098       * 
  1099       * @param event Key event
  1100       */
  1101      @Override
  1102      public void keyTyped(final KeyEvent event) {
  1103          //Ignore.
                 /* 
    P/P           *  Method: void keyTyped(KeyEvent)
                  */
  1104          }
  1105  
  1106      /** 
  1107       * {@inheritDoc}
  1108       * 
  1109       * @param event Key event
  1110       */
  1111      @Override
  1112      public void keyPressed(final KeyEvent event) {
                 /* 
    P/P           *  Method: void keyPressed(KeyEvent)
                  * 
                  *  Preconditions:
                  *    init'ed(this.quickCopy)
                  *    (soft) event != null
                  *    (soft) this.textPane != null
                  * 
                  *  Test Vectors:
                  *    this.quickCopy: {1}, {0}
                  *    java.awt.event.KeyEvent:getKeyCode(...)@1113: {-231..66, 68..232-1}, {67}
                  */
  1113          if (!quickCopy && (event.getModifiers() & UIUtilities.getCtrlMask()) !=
  1114                  0 &&
  1115                  event.getKeyCode() == KeyEvent.VK_C) {
  1116              getTextPane().copy();
  1117          }
  1118  
  1119      }
  1120  
  1121      /** 
  1122       * {@inheritDoc}
  1123       * 
  1124       * @param event Key event
  1125       */
  1126      @Override
  1127      public void keyReleased(final KeyEvent event) {
  1128          //Ignore.
                 /* 
    P/P           *  Method: void keyReleased(KeyEvent)
                  */
  1129          }
  1130  
  1131      /**
  1132       * Gets the search bar.
  1133       *
  1134       * @return the frames search bar
  1135       */
  1136      public final SwingSearchBar getSearchBar() {
                 /* 
    P/P           *  Method: SwingSearchBar getSearchBar()
                  * 
                  *  Preconditions:
                  *    init'ed(this.searchBar)
                  * 
                  *  Postconditions:
                  *    return_value == this.searchBar
                  *    init'ed(return_value)
                  */
  1137          return searchBar;
  1138      }
  1139  
  1140      /** {@inheritDoc} */
  1141      @Override
  1142      public void configChanged(final String domain,
  1143              final String key) {
                 /* 
    P/P           *  Method: void configChanged(String, String)
                  * 
                  *  Preconditions:
                  *    (soft) this.frameParent != null
                  *    (soft) init'ed(this.textPane)
                  * 
                  *  Presumptions:
                  *    com.dmdirc.FrameContainer:getConfigManager(...)@1156 != null
                  *    com.dmdirc.FrameContainer:getConfigManager(...)@1159 != null
                  *    com.dmdirc.FrameContainer:getConfigManager(...)@770 != null
                  * 
                  *  Postconditions:
                  *    possibly_updated(this.frameBufferSize)
                  *    possibly_updated(this.quickCopy)
                  * 
                  *  Test Vectors:
                  *    this.textPane: Addr_Set{null}, Inverse{null}
                  *    com.dmdirc.FrameContainer:getConfigManager(...)@770: Inverse{null}, Addr_Set{null}
                  *    java.lang.String:equals(...)@1148: {0}, {1}
                  *    java.lang.String:equals(...)@1149: {0}, {1}
                  *    java.lang.String:equals(...)@1152: {0}, {1}
                  *    java.lang.String:equals(...)@1155: {0}, {1}
                  *    java.lang.String:equals(...)@1158: {0}, {1}
                  */
  1144          if (getConfigManager() == null) {
  1145              return;
  1146          }
  1147  
  1148          if ("ui".equals(domain)) {
  1149              if ("foregroundcolour".equals(key) && getTextPane() != null) {
  1150                  getTextPane().setForeground(getConfigManager().
  1151                          getOptionColour("ui", "foregroundcolour"));
  1152              } else if ("backgroundcolour".equals(key) && getTextPane() != null) {
  1153                  getTextPane().setBackground(getConfigManager().
  1154                          getOptionColour("ui", "backgroundcolour"));
  1155              } else if ("frameBufferSize".equals(key)) {
  1156                  frameBufferSize = getContainer().getConfigManager().
  1157                          getOptionInt("ui", "frameBufferSize");
  1158              } else if ("quickCopy".equals(key)) {
  1159                  quickCopy = getContainer().getConfigManager().
  1160                          getOptionBool("ui", "quickCopy");
  1161              }
  1162          }
  1163      }
  1164  }








SofCheck Inspector Build Version : 2.17854
TextFrame.java 2009-Jun-25 01:54:24
TextFrame.class 2009-Sep-02 17:04:17
TextFrame$1.class 2009-Sep-02 17:04:17
TextFrame$10.class 2009-Sep-02 17:04:17
TextFrame$11.class 2009-Sep-02 17:04:17
TextFrame$11$1.class 2009-Sep-02 17:04:17
TextFrame$12.class 2009-Sep-02 17:04:17
TextFrame$13.class 2009-Sep-02 17:04:17
TextFrame$14.class 2009-Sep-02 17:04:17
TextFrame$15.class 2009-Sep-02 17:04:17
TextFrame$16.class 2009-Sep-02 17:04:17
TextFrame$17.class 2009-Sep-02 17:04:17
TextFrame$18.class 2009-Sep-02 17:04:17
TextFrame$19.class 2009-Sep-02 17:04:17
TextFrame$2.class 2009-Sep-02 17:04:17
TextFrame$20.class 2009-Sep-02 17:04:17
TextFrame$21.class 2009-Sep-02 17:04:17
TextFrame$3.class 2009-Sep-02 17:04:17
TextFrame$4.class 2009-Sep-02 17:04:17
TextFrame$5.class 2009-Sep-02 17:04:17
TextFrame$6.class 2009-Sep-02 17:04:17
TextFrame$7.class 2009-Sep-02 17:04:17
TextFrame$8.class 2009-Sep-02 17:04:17
TextFrame$9.class 2009-Sep-02 17:04:17
TextFrame$MouseClickType.class 2009-Sep-02 17:04:17