File Source: Tree.java

         /* 
    P/P   *  Method: com.dmdirc.addons.ui_swing.framemanager.tree.Tree__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.framemanager.tree;
    23  
    24  import com.dmdirc.addons.ui_swing.UIUtilities;
    25  import com.dmdirc.config.IdentityManager;
    26  import com.dmdirc.interfaces.ConfigChangeListener;
    27  import com.dmdirc.addons.ui_swing.actions.CloseFrameContainerAction;
    28  import com.dmdirc.addons.ui_swing.components.TreeScroller;
    29  import com.dmdirc.addons.ui_swing.components.frames.TextFrame;
    30  
    31  import java.awt.event.MouseEvent;
    32  import java.awt.event.MouseListener;
    33  import java.awt.event.MouseMotionListener;
    34  
    35  import javax.swing.BorderFactory;
    36  import javax.swing.JComponent;
    37  import javax.swing.JMenuItem;
    38  import javax.swing.JPopupMenu;
    39  import javax.swing.JTree;
    40  import javax.swing.tree.TreeModel;
    41  import javax.swing.tree.TreePath;
    42  import javax.swing.tree.TreeSelectionModel;
    43  
    44  import net.miginfocom.layout.PlatformDefaults;
    45  
    46  /**
    47   * Specialised JTree for the frame manager.
    48   */
    49  public class Tree extends JTree implements MouseMotionListener,
    50          ConfigChangeListener, MouseListener {
    51  
    52      /**
    53       * A version number for this class. It should be changed whenever the class
    54       * structure is changed (or anything else that would prevent serialized
    55       * objects being unserialized with the new class).
    56       */
    57      private static final long serialVersionUID = 1;
    58      /** Drag selection enabled? */
    59      private boolean dragSelect;
    60      /** Drag button 1? */
    61      private boolean dragButton;
    62      /** Tree frame manager. */
    63      private TreeFrameManager manager;
    64      /** Current selection path. */
    65      private TreePath path;
    66  
    67      /**
    68       * Specialised JTree for frame manager.
    69       *
    70       * @param manager Frame manager
    71       * @param model tree model.
    72       */
    73      public Tree(final TreeFrameManager manager, final TreeModel model) {
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.framemanager.tree.Tree(TreeFrameManager, TreeModel)
                  * 
                  *  Preconditions:
                  *    init'ed(com/dmdirc/config/IdentityManager.globalconfig)
                  *    (soft) init'ed(com.dmdirc.config.ConfigManager$1__static_init.new int[](ConfigManager$1__static_init#1)[...])
                  * 
                  *  Presumptions:
                  *    (int) (net.miginfocom.layout.UnitValue:getValue(...)@88) in {-231..232-1}
                  *    com.dmdirc.addons.ui_swing.framemanager.tree.Tree:getInputMap(...)@79 != null
                  *    com.dmdirc.addons.ui_swing.framemanager.tree.Tree:getInputMap(...)@80 != null
                  *    com.dmdirc.addons.ui_swing.framemanager.tree.Tree:getInputMap(...)@81 != null
                  *    com.dmdirc.addons.ui_swing.framemanager.tree.Tree:getInputMap(...)@82 != null
                  *    ...
                  * 
                  *  Postconditions:
                  *    com/dmdirc/config/IdentityManager.globalconfig != null
                  *    java.lang.StringBuilder:toString(...)._tainted == 0
                  *    new ArrayList(getSources#1) num objects == 0
                  *    new ConfigManager(getGlobalConfig#1) num objects == 0
                  *    new MapList(ConfigManager#1) num objects == 0
                  *    init'ed(this.dragSelect)
                  *    this.manager == manager
                  *    init'ed(this.manager)
                  *    new ArrayList(getSources#1) num objects <= 1
                  *    new ConfigManager(getGlobalConfig#1) num objects == new ArrayList(getSources#1) num objects
                  *    ...
                  */
    74          super(model);
    75  
    76          this.manager = manager;
    77  
    78          putClientProperty("JTree.lineStyle", "Angled");
    79          getInputMap().setParent(null);
    80          getInputMap(JComponent.WHEN_FOCUSED).clear();
    81          getInputMap(JComponent.WHEN_ANCESTOR_OF_FOCUSED_COMPONENT).clear();
    82          getInputMap(JComponent.WHEN_IN_FOCUSED_WINDOW).clear();
    83          getSelectionModel().setSelectionMode(TreeSelectionModel.SINGLE_TREE_SELECTION);
    84          setRootVisible(false);
    85          setRowHeight(0);
    86          setShowsRootHandles(false);
    87          setOpaque(true);
    88          setBorder(BorderFactory.createEmptyBorder(
    89                  (int) PlatformDefaults.getUnitValueX("related").getValue(),
    90                  (int) PlatformDefaults.getUnitValueX("related").getValue(),
    91                  (int) PlatformDefaults.getUnitValueX("related").getValue(),
    92                  (int) PlatformDefaults.getUnitValueX("related").getValue()));
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.framemanager.tree.Tree$1(Tree, JTree)
                  */
    93          new TreeScroller(this) {
    94  
    95              /** {@inheritDoc} */
    96              @Override
    97              protected void setPath(final TreePath path) {
                         /* 
    P/P                   *  Method: void setPath(TreePath)
                          * 
                          *  Preconditions:
                          *    path != null
                          * 
                          *  Presumptions:
                          *    javax.swing.tree.TreePath:getLastPathComponent(...).frameContainer@99 != null
                          *    javax.swing.tree.TreePath:getLastPathComponent(...)@99 != null
                          */
    98                  super.setPath(path);
    99                  ((TreeViewNode) path.getLastPathComponent()).getFrameContainer().activateFrame();
   100              }
   101          };
   102          setFocusable(false);
   103  
   104          dragSelect = IdentityManager.getGlobalConfig().getOptionBool("treeview",
   105                  "dragSelection");
   106          IdentityManager.getGlobalConfig().addChangeListener("treeview",
   107                  "dragSelection", this);
   108  
   109          addMouseListener(this);
   110          addMouseMotionListener(this);
   111      }
   112  
   113      /**
   114       * Set path.
   115       *
   116       * @param path Path
   117       */
   118      public void setTreePath(final TreePath path) {
                 /* 
    P/P           *  Method: void setTreePath(TreePath)
                  * 
                  *  Postconditions:
                  *    this.path == path
                  *    init'ed(this.path)
                  */
   119          this.path = path;
                 /* 
    P/P           *  Method: void com.dmdirc.addons.ui_swing.framemanager.tree.Tree$2(Tree, TreePath)
                  * 
                  *  Postconditions:
                  *    this.val$path == Param_2
                  *    init'ed(this.val$path)
                  */
   120          UIUtilities.invokeLater(new Runnable() {
   121  
   122              @Override
   123              public void run() {
                         /* 
    P/P                   *  Method: void run()
                          */
   124                  setSelectionPath(path);
   125              }
   126          });
   127      }
   128  
   129      /**
   130       * Returns the node for the specified location, returning null if rollover
   131       * is disabled or there is no node at the specified location.
   132       *
   133       * @param x x coordiantes
   134       * @param y y coordiantes
   135       *
   136       * @return node or null
   137       */
   138      public TreeViewNode getNodeForLocation(final int x,
   139              final int y) {
                 /* 
    P/P           *  Method: TreeViewNode getNodeForLocation(int, int)
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.addons.ui_swing.framemanager.tree.Tree:getPathForLocation(...)@141: Addr_Set{null}, Inverse{null}
                  */
   140          TreeViewNode node = null;
   141          final TreePath selectedPath = getPathForLocation(x, y);
   142          if (selectedPath != null) {
   143              node = (TreeViewNode) selectedPath.getLastPathComponent();
   144          }
   145          return node;
   146      }
   147  
   148      /** {@inheritDoc} */
   149      @Override
   150      public void configChanged(final String domain, final String key) {
                 /* 
    P/P           *  Method: void configChanged(String, String)
                  * 
                  *  Preconditions:
                  *    init'ed(com/dmdirc/config/IdentityManager.globalconfig)
                  *    (soft) init'ed(com.dmdirc.config.ConfigManager$1__static_init.new int[](ConfigManager$1__static_init#1)[...])
                  * 
                  *  Postconditions:
                  *    com/dmdirc/config/IdentityManager.globalconfig == One-of{old com/dmdirc/config/IdentityManager.globalconfig, &amp;new ConfigManager(getGlobalConfig#1)}
                  *    com/dmdirc/config/IdentityManager.globalconfig != null
                  *    java.lang.StringBuilder:toString(...)._tainted == 0
                  *    init'ed(this.dragSelect)
                  *    new ArrayList(getSources#1) num objects <= 1
                  *    new ConfigManager(getGlobalConfig#1) num objects == new ArrayList(getSources#1) num objects
                  *    new MapList(ConfigManager#1) num objects == new ArrayList(getSources#1) num objects
                  *    new ConfigManager(getGlobalConfig#1).channel == &amp;java.lang.StringBuilder:toString(...)
                  *    init'ed(new ConfigManager(getGlobalConfig#1).file)
                  *    new ConfigManager(getGlobalConfig#1).ircd == &amp;""
                  *    ...
                  */
   151          dragSelect = IdentityManager.getGlobalConfig().getOptionBool("treeview",
   152                  "dragSelection");
   153      }
   154  
   155      /** 
   156       * {@inheritDoc}
   157       * 
   158       * @param e Mouse event
   159       */
   160      @Override
   161      public void mouseDragged(final MouseEvent e) {
                 /* 
    P/P           *  Method: void mouseDragged(MouseEvent)
                  * 
                  *  Preconditions:
                  *    init'ed(this.dragSelect)
                  *    this.manager != null
                  *    this.manager.nodes != null
                  *    this.manager.tree != null
                  *    (soft) e != null
                  *    (soft) init'ed(this.dragButton)
                  * 
                  *  Presumptions:
                  *    javax.swing.tree.TreePath:getLastPathComponent(...).frameContainer@165 != null
                  *    javax.swing.tree.TreePath:getLastPathComponent(...)@165 != null
                  * 
                  *  Test Vectors:
                  *    this.dragButton: {0}, {1}
                  *    this.dragSelect: {0}, {1}
                  */
   162          if (dragSelect && dragButton) {
   163              final TreeViewNode node = getNodeForLocation(e.getX(), e.getY());
   164              if (node != null) {
   165                  ((TreeViewNode) new TreePath(node.getPath()).getLastPathComponent()).getFrameContainer().activateFrame();
   166              }
   167          }
   168          manager.checkRollover(e);
   169      }
   170  
   171      /** 
   172       * {@inheritDoc}
   173       * 
   174       * @param e Mouse event
   175       */
   176      @Override
   177      public void mouseMoved(final MouseEvent e) {
                 /* 
    P/P           *  Method: void mouseMoved(MouseEvent)
                  * 
                  *  Preconditions:
                  *    this.manager != null
                  *    this.manager.nodes != null
                  *    this.manager.tree != null
                  */
   178          manager.checkRollover(e);
   179      }
   180  
   181      /** 
   182       * {@inheritDoc}
   183       * 
   184       * @param e Mouse event
   185       */
   186      @Override
   187      public void mouseClicked(MouseEvent e) {
                 /* 
    P/P           *  Method: void mouseClicked(MouseEvent)
                  * 
                  *  Preconditions:
                  *    e != null
                  */
   188          processMouseEvents(e);
   189      }
   190  
   191      /** 
   192       * {@inheritDoc}
   193       * 
   194       * @param e Mouse event
   195       */
   196      @Override
   197      public void mousePressed(MouseEvent e) {
                 /* 
    P/P           *  Method: void mousePressed(MouseEvent)
                  * 
                  *  Preconditions:
                  *    e != null
                  * 
                  *  Presumptions:
                  *    javax.swing.tree.TreePath:getLastPathComponent(...).frameContainer@202 != null
                  *    javax.swing.tree.TreePath:getLastPathComponent(...)@202 != null
                  * 
                  *  Postconditions:
                  *    possibly_updated(this.dragButton)
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.addons.ui_swing.framemanager.tree.Tree:getPathForLocation(...)@200: Addr_Set{null}, Inverse{null}
                  *    java.awt.event.MouseEvent:getButton(...)@198: {-231..0, 2..232-1}, {1}
                  */
   198          if (e.getButton() == MouseEvent.BUTTON1) {
   199              dragButton = true;
   200              final TreePath selectedPath = getPathForLocation(e.getX(), e.getY());
   201              if (selectedPath != null) {
   202                  ((TreeViewNode) selectedPath.getLastPathComponent()).getFrameContainer().activateFrame();
   203              }
   204          }
   205          processMouseEvents(e);
   206      }
   207  
   208      /** 
   209       * {@inheritDoc}
   210       * 
   211       * @param e Mouse event
   212       */
   213      @Override
   214      public void mouseReleased(MouseEvent e) {
                 /* 
    P/P           *  Method: void mouseReleased(MouseEvent)
                  * 
                  *  Preconditions:
                  *    e != null
                  * 
                  *  Postconditions:
                  *    this.dragButton == 0
                  */
   215          dragButton = false;
   216          processMouseEvents(e);
   217      }
   218  
   219      /** 
   220       * {@inheritDoc}
   221       * 
   222       * @param e Mouse event
   223       */
   224      @Override
   225      public void mouseEntered(MouseEvent e) {
   226          //Ignore
             /* 
    P/P       *  Method: void mouseEntered(MouseEvent)
              */
   227      }
   228  
   229      /** 
   230       * {@inheritDoc}
   231       * 
   232       * @param e Mouse event
   233       */
   234      @Override
   235      public void mouseExited(MouseEvent e) {
                 /* 
    P/P           *  Method: void mouseExited(MouseEvent)
                  * 
                  *  Preconditions:
                  *    this.manager != null
                  *    this.manager.nodes != null
                  *    this.manager.tree != null
                  */
   236          manager.checkRollover(null);
   237      }
   238  
   239      /**
   240       * Processes every mouse button event to check for a popup trigger.
   241       * @param e mouse event
   242       */
   243      public void processMouseEvents(final MouseEvent e) {
                 /* 
    P/P           *  Method: void processMouseEvents(MouseEvent)
                  * 
                  *  Preconditions:
                  *    e != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.FrameContainer:getFrame(...)@247 != null
                  *    com.dmdirc.addons.ui_swing.components.frames.TextFrame:getPopupMenu(...)@249 != null
                  *    javax.swing.tree.TreePath:getLastPathComponent(...).frameContainer@247 != null
                  *    javax.swing.tree.TreePath:getLastPathComponent(...)@247 != null
                  * 
                  *  Test Vectors:
                  *    com.dmdirc.addons.ui_swing.framemanager.tree.Tree:getPathForLocation(...)@244: Addr_Set{null}, Inverse{null}
                  *    java.awt.event.MouseEvent:isPopupTrigger(...)@246: {0}, {1}
                  *    javax.swing.JPopupMenu:getComponentCount(...)@251: {-231..0}, {1..232-1}
                  */
   244          final TreePath localPath = getPathForLocation(e.getX(), e.getY());
   245          if (localPath != null) {
   246              if (e.isPopupTrigger()) {
   247                  final TextFrame frame = (TextFrame) ((TreeViewNode) localPath.getLastPathComponent()).getFrameContainer().
   248                          getFrame();
   249                  final JPopupMenu popupMenu = frame.getPopupMenu(null, "");
   250                  frame.addCustomPopupItems(popupMenu);
   251                  if (popupMenu.getComponentCount() > 0) {
   252                      popupMenu.addSeparator();
   253                  }
   254                  popupMenu.add(new JMenuItem(new CloseFrameContainerAction(frame.getContainer())));
   255                  popupMenu.show(this, e.getX(), e.getY());
   256              }
   257          }
   258      }
   259  }








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