File Source: PreferencesCategory.java

     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.config.prefs;
    23  
    24  import com.dmdirc.util.ListenerList;
    25  
    26  import java.util.ArrayList;
    27  import java.util.List;
    28  
    29  /**
    30   * Represents one category of preferences. Categories can contain 0 or more
    31   * subcategories, and either 0 or more PreferencesSettings or exactly 1
    32   * PreferencesInterface object.
    33   * 
    34   * @author chris
    35   */
    36  public class PreferencesCategory {
    37  
    38      /** A logger for this class. */
             /* 
    P/P       *  Method: com.dmdirc.config.prefs.PreferencesCategory__static_init
              * 
              *  Postconditions:
              *    init'ed(LOGGER)
              */
    39      private static final java.util.logging.Logger LOGGER = java.util.logging
    40              .Logger.getLogger(PreferencesCategory.class.getName());
    41          
    42      /** The title (name) of this category. */
    43      private final String title;
    44      
    45      /** A description of this category. */
    46      private final String description;
    47  
    48      /** The icon to use for this category. */
    49      private final String icon;
    50      
    51      /** Whether or not this category is inline. */
    52      private boolean isInline = false;
    53      
    54      /** Whether or not to show inline categories before settings. */
    55      private boolean inlineBefore = true;
    56  
    57      /** Our parent category, if known. */
    58      private PreferencesCategory parent;
    59      
    60      /** A list of settings in this category. */
    61      private final List<PreferencesSetting> settings = new ArrayList<PreferencesSetting>();
    62      
    63      /** A list of subcategories of this category. */
    64      private final List<PreferencesCategory> subcats = new ArrayList<PreferencesCategory>();
    65      
    66      /** The replacement object to use for this category. */
    67      private final PreferencesInterface object;
    68      
    69      /** A list of listeners who are interested in this category. */
    70      private final ListenerList listeners = new ListenerList();
    71  
    72      /**
    73       * Creates a new preferences category that contains settings.
    74       * 
    75       * @param title The title of this preferences category
    76       * @param description The description of this category
    77       */
    78      public PreferencesCategory(final String title, final String description) {
                 /* 
    P/P           *  Method: void com.dmdirc.config.prefs.PreferencesCategory(String, String)
                  * 
                  *  Postconditions:
                  *    this.description == description
                  *    init'ed(this.description)
                  *    this.icon == null
                  *    this.object == null
                  *    this.inlineBefore == 1
                  *    new ArrayList(PreferencesCategory#1) num objects == 1
                  *    new ArrayList(PreferencesCategory#2) num objects == 1
                  *    new ListenerList(PreferencesCategory#3) num objects == 1
                  *    this.isInline == 0
                  *    this.listeners == &amp;new ListenerList(PreferencesCategory#3)
                  *    ...
                  */
    79          this(title, description, null, null);
    80      }
    81  
    82      /**
    83       * Creates a new preferences category that contains settings.
    84       *
    85       * @since 0.6.3m1
    86       * @param title The title of this preferences category
    87       * @param description The description of this category
    88       * @param icon The icon to use for this category
    89       */
    90      public PreferencesCategory(final String title, final String description,
    91              final String icon) {
                 /* 
    P/P           *  Method: void com.dmdirc.config.prefs.PreferencesCategory(String, String, String)
                  * 
                  *  Postconditions:
                  *    this.description == description
                  *    init'ed(this.description)
                  *    this.icon == icon
                  *    init'ed(this.icon)
                  *    this.inlineBefore == 1
                  *    new ArrayList(PreferencesCategory#1) num objects == 1
                  *    new ArrayList(PreferencesCategory#2) num objects == 1
                  *    new ListenerList(PreferencesCategory#3) num objects == 1
                  *    this.isInline == 0
                  *    this.listeners == &amp;new ListenerList(PreferencesCategory#3)
                  *    ...
                  */
    92          this(title, description, icon, null);
    93      }
    94  
    95      /**
    96       * Creates a new preferences category that contains an object.
    97       *
    98       * @param title The title of this preferences category
    99       * @param description The description of this category
   100       * @param object The replacement object for this category
   101       */
   102      public PreferencesCategory(final String title, final String description,
   103              final PreferencesInterface object) {
                 /* 
    P/P           *  Method: void com.dmdirc.config.prefs.PreferencesCategory(String, String, PreferencesInterface)
                  * 
                  *  Postconditions:
                  *    this.description == description
                  *    init'ed(this.description)
                  *    this.icon == null
                  *    this.inlineBefore == 1
                  *    new ArrayList(PreferencesCategory#1) num objects == 1
                  *    new ArrayList(PreferencesCategory#2) num objects == 1
                  *    new ListenerList(PreferencesCategory#3) num objects == 1
                  *    this.isInline == 0
                  *    this.listeners == &amp;new ListenerList(PreferencesCategory#3)
                  *    this.object == object
                  *    ...
                  */
   104          this(title, description, null, object);
   105      }
   106      
   107      /**
   108       * Creates a new preferences category that contains an object.
   109       *
   110       * @since 0.6.3m1
   111       * @param title The title of this preferences category
   112       * @param description The description of this category
   113       * @param icon The icon to use for this category
   114       * @param object The replacement object for this category
   115       */
   116      public PreferencesCategory(final String title, final String description,
                     /* 
    P/P               *  Method: void com.dmdirc.config.prefs.PreferencesCategory(String, String, String, PreferencesInterface)
                      * 
                      *  Postconditions:
                      *    this.description == description
                      *    init'ed(this.description)
                      *    this.icon == icon
                      *    init'ed(this.icon)
                      *    this.inlineBefore == 1
                      *    new ArrayList(PreferencesCategory#1) num objects == 1
                      *    new ArrayList(PreferencesCategory#2) num objects == 1
                      *    new ListenerList(PreferencesCategory#3) num objects == 1
                      *    this.isInline == 0
                      *    this.listeners == &amp;new ListenerList(PreferencesCategory#3)
                      *    ...
                      */
   117              final String icon, final PreferencesInterface object) {
   118          this.title = title;
   119          this.description = description;
   120          this.icon = icon;
   121          this.object = object;
   122      }
   123      
   124      /**
   125       * Sets this as an inline category.
   126       * 
   127       * @return A reference to this category, for convenience
   128       */
   129      public PreferencesCategory setInline() {
                 /* 
    P/P           *  Method: PreferencesCategory setInline()
                  * 
                  *  Postconditions:
                  *    return_value == this
                  *    return_value != null
                  *    this.isInline == 1
                  */
   130          isInline = true;
   131          return this;
   132      }
   133      
   134      /**
   135       * Sets this category to show inline categories after settings, rather than
   136       * before.
   137       * 
   138       * @return A reference to this category, for convenience
   139       */
   140      public PreferencesCategory setInlineAfter() {
                 /* 
    P/P           *  Method: PreferencesCategory setInlineAfter()
                  * 
                  *  Postconditions:
                  *    return_value == this
                  *    return_value != null
                  *    this.inlineBefore == 0
                  */
   141          inlineBefore = false;
   142          return this;
   143      }
   144      
   145      /**
   146       * Determines if this category is meant to be displayed inline or not.
   147       * 
   148       * @return True if this category should be shown inline, false otherwise
   149       */
   150      public boolean isInline() {
                 /* 
    P/P           *  Method: bool isInline()
                  * 
                  *  Preconditions:
                  *    init'ed(this.isInline)
                  * 
                  *  Postconditions:
                  *    return_value == this.isInline
                  *    init'ed(return_value)
                  */
   151          return isInline;
   152      }
   153      
   154      /**
   155       * Determines whether this category wants inline subcats to be displayed
   156       * before the settings, or after.
   157       * 
   158       * @return True if subcats should be displayed first, false otherwise.
   159       */
   160      public boolean isInlineBefore() {
                 /* 
    P/P           *  Method: bool isInlineBefore()
                  * 
                  *  Preconditions:
                  *    init'ed(this.inlineBefore)
                  * 
                  *  Postconditions:
                  *    return_value == this.inlineBefore
                  *    init'ed(return_value)
                  */
   161          return inlineBefore;
   162      }
   163      
   164      /**
   165       * Adds the specified setting to this category.
   166       * 
   167       * @param setting The setting to be added
   168       */
   169      public void addSetting(final PreferencesSetting setting) {
                 /* 
    P/P           *  Method: void addSetting(PreferencesSetting)
                  * 
                  *  Preconditions:
                  *    this.object == null
                  *    this.settings != null
                  */
   170          if (hasObject()) {
   171              throw new IllegalArgumentException("Can't add settings to a " +
   172                      "category that uses a replacement object");
   173          }
   174          
   175          settings.add(setting);
   176      }
   177      
   178      /**
   179       * Adds the specified subcategory to this category.
   180       * 
   181       * @param subcategory The category to be asdded
   182       */
   183      public void addSubCategory(final PreferencesCategory subcategory) {
                 /* 
    P/P           *  Method: void addSubCategory(PreferencesCategory)
                  * 
                  *  Preconditions:
                  *    subcategory != null
                  *    init'ed(this.isInline)
                  *    this.subcats != null
                  *    (soft) subcategory.isInline == 1
                  * 
                  *  Postconditions:
                  *    subcategory.parent == this
                  *    subcategory.parent != null
                  * 
                  *  Test Vectors:
                  *    this.isInline: {0}, {1}
                  */
   184          if (isInline() && !subcategory.isInline()) {
   185              throw new IllegalArgumentException("Can't add non-inline " +
   186                      "subcategories to inline ones");
   187          }
   188  
   189          subcategory.setParent(this);
   190          subcats.add(subcategory);
   191      }
   192  
   193      /**
   194       * Retrieves the description of this category.
   195       * 
   196       * @return This category's description
   197       */
   198      public String getDescription() {
                 /* 
    P/P           *  Method: String getDescription()
                  * 
                  *  Postconditions:
                  *    return_value == this.description
                  *    init'ed(return_value)
                  */
   199          return description;
   200      }
   201  
   202      /**
   203       * Retrieves the settings in this category.
   204       * 
   205       * @return This category's settings
   206       */
   207      public List<PreferencesSetting> getSettings() {
                 /* 
    P/P           *  Method: List getSettings()
                  * 
                  *  Postconditions:
                  *    return_value == this.settings
                  *    init'ed(return_value)
                  */
   208          return settings;
   209      }
   210  
   211      /**
   212       * Retrieves the subcategories of this category.
   213       * 
   214       * @return This category's subcategories
   215       */
   216      public List<PreferencesCategory> getSubcats() {
                 /* 
    P/P           *  Method: List getSubcats()
                  * 
                  *  Postconditions:
                  *    return_value == this.subcats
                  *    init'ed(return_value)
                  */
   217          return subcats;
   218      }
   219  
   220      /**
   221       * Retrieves the title of this category.
   222       * 
   223       * @return This category's title
   224       */
   225      public String getTitle() {
                 /* 
    P/P           *  Method: String getTitle()
                  * 
                  *  Postconditions:
                  *    return_value == this.title
                  *    init'ed(return_value)
                  */
   226          return title;
   227      }
   228  
   229      /**
   230       * Retrieves the icon to use for this category.
   231       *
   232       * @return This category's icon
   233       * @since 0.6.3m1
   234       */
   235      public String getIcon() {
                 /* 
    P/P           *  Method: String getIcon()
                  * 
                  *  Postconditions:
                  *    return_value == this.icon
                  *    init'ed(return_value)
                  */
   236          return icon;
   237      }
   238      
   239      /**
   240       * Determines if this category has a replacement object.
   241       * 
   242       * @return True if the category has a replacement object, false otherwise
   243       * @see #getObject()
   244       */
   245      public boolean hasObject() {
                 /* 
    P/P           *  Method: bool hasObject()
                  * 
                  *  Postconditions:
                  *    init'ed(return_value)
                  */
   246          return object != null;
   247      }
   248      
   249      /**
   250       * Retrieves this category's replacement object.
   251       * 
   252       * @return This category's replacement object.
   253       * @see #hasObject()
   254       */
   255      public PreferencesInterface getObject() {
                 /* 
    P/P           *  Method: PreferencesInterface getObject()
                  * 
                  *  Postconditions:
                  *    return_value == this.object
                  *    init'ed(return_value)
                  */
   256          return object;
   257      }
   258  
   259      /**
   260       * Retrieves the full path of this category. A category's path is the name
   261       * of each of its parent categories, starting with the furthest up the
   262       * hierarchy, separated by '→' characters.
   263       *
   264       * @return This category's path
   265       * @since 0.6.3m1
   266       */
   267      public String getPath() {
                 /* 
    P/P           *  Method: String getPath()
                  * 
                  *  Preconditions:
                  *    init'ed(this.parent)
                  *    (soft) init'ed(this...parent)
                  * 
                  *  Postconditions:
                  *    java.lang.StringBuilder:toString(...)._tainted == this.title._tainted | One-of{0, this...title._tainted | One-of{0, this...title._tainted | One-of{0, this...title._tainted | One-of{0, this...title._tainted}}}}
                  *    init'ed(java.lang.StringBuilder:toString(...)._tainted)
                  *    return_value == &amp;java.lang.StringBuilder:toString(...)
                  */
   268          return (parent == null ? "" : parent.getPath() + " → ") + getTitle();
   269      }
   270  
   271      /**
   272       * Sets this category's parent.
   273       *
   274       * @param parent The parent of this category
   275       * @since 0.6.3m1
   276       */
   277      public void setParent(final PreferencesCategory parent) {
                 /* 
    P/P           *  Method: void setParent(PreferencesCategory)
                  * 
                  *  Postconditions:
                  *    this.parent == parent
                  *    init'ed(this.parent)
                  */
   278          this.parent = parent;
   279      }
   280  
   281      /**
   282       * Retrieves the parent of this category.
   283       *
   284       * @return This category's parent, or null if it's an orphan
   285       * @since 0.6.3m1
   286       */
   287      public PreferencesCategory getParent() {
                 /* 
    P/P           *  Method: PreferencesCategory getParent()
                  * 
                  *  Preconditions:
                  *    init'ed(this.parent)
                  * 
                  *  Postconditions:
                  *    return_value == this.parent
                  *    init'ed(return_value)
                  */
   288          return parent;
   289      }
   290  
   291      /**
   292       * Saves all the settings in this category.
   293       *
   294       * @return Is a restart needed after saving?
   295       */
   296      public boolean save() {
                 /* 
    P/P           *  Method: bool save()
                  * 
                  *  Preconditions:
                  *    this.settings != null
                  *    this.subcats != null
                  *    (soft) init'ed(com.dmdirc.config.ConfigManager$1__static_init.new int[](ConfigManager$1__static_init#1)[...])
                  *    (soft) com/dmdirc/config/IdentityManager.config != null
                  *    (soft) com/dmdirc/config/IdentityManager.config.file != null
                  *    (soft) com/dmdirc/config/IdentityManager.config.listeners != null
                  *    (soft) com/dmdirc/config/IdentityManager.config.myTarget != null
                  *    (soft) init'ed(com/dmdirc/config/IdentityManager.config.myTarget.type)
                  *    (soft) init'ed(com/dmdirc/config/IdentityManager.config.globalConfig)
                  * 
                  *  Presumptions:
                  *    java.util.Iterator:next(...)@300 != null
                  *    java.util.Iterator:next(...)@307 != null
                  *    java.util.logging.Logger:getLogger(...)@39 != null
                  * 
                  *  Postconditions:
                  *    init'ed(com/dmdirc/config/IdentityManager.config.globalConfig)
                  *    possibly_updated(com/dmdirc/config/IdentityManager.config.needSave)
                  *    java.lang.StringBuilder:toString(...)._tainted == 0
                  *    init'ed(return_value)
                  *    init'ed(new ArrayList(getSources#1) num objects)
                  *    new ArrayList(getSources#1) num objects == undefined
                  *    new ArrayList(getSources#1) num objects == 0, if init'ed
                  *    new ConfigManager(setOption#2) num objects == new ArrayList(getSources#1) num objects
                  *    new MapList(ConfigManager#1) num objects == new ArrayList(getSources#1) num objects
                  *    init'ed(new ConfigManager(setOption#2) num objects)
                  *    ...
                  * 
                  *  Test Vectors:
                  *    java.util.Iterator:hasNext(...)@300: {0}, {1}
                  *    java.util.Iterator:hasNext(...)@307: {0}, {1}
                  *    setting.restartNeeded@302: {0}, {1}
                  */
   297          LOGGER.fine(getTitle() + ": save method called");
   298  
   299          boolean restart = false;
   300          for (PreferencesSetting setting : settings) {
   301              LOGGER.finest(getTitle() + ": saving setting '" + setting.getTitle() + "'");
   302              if (setting.save() && setting.isRestartNeeded()) {
   303                  restart = true;
   304              }
   305          }
   306  
   307          for (PreferencesCategory child : getSubcats()) {
   308              restart |= child.save();
   309          }
   310  
   311          return restart;
   312      }
   313  
   314      /**
   315       * Dismisses all the settings in this category.
   316       */
   317      public void dismiss() {
                 /* 
    P/P           *  Method: void dismiss()
                  * 
                  *  Preconditions:
                  *    this.settings != null
                  *    this.subcats != null
                  * 
                  *  Presumptions:
                  *    child.settings@322 != null
                  *    child.subcats@322 != null
                  *    java.util.Iterator:next(...)@318 != null
                  *    java.util.Iterator:next(...)@322 != null
                  *    setting.listeners@318 != null
                  * 
                  *  Test Vectors:
                  *    java.util.Iterator:hasNext(...)@318: {0}, {1}
                  *    java.util.Iterator:hasNext(...)@322: {0}, {1}
                  */
   318          for (PreferencesSetting setting : settings) {
   319              setting.dismiss();
   320          }
   321  
   322          for (PreferencesCategory child : getSubcats()) {
   323              child.dismiss();
   324          }
   325      }
   326      
   327      /**
   328       * Registers a change listener for this category.
   329       * 
   330       * @param listener The listener to be added
   331       */
   332      public void addChangeListener(final CategoryChangeListener listener) {
                 /* 
    P/P           *  Method: void addChangeListener(CategoryChangeListener)
                  * 
                  *  Preconditions:
                  *    this.listeners != null
                  */
   333          listeners.add(CategoryChangeListener.class, listener);
   334      }
   335      
   336      /**
   337       * Removes a change listener from this category.
   338       * 
   339       * @param listener The listener to be added
   340       */
   341      public void removeChangeListener(final CategoryChangeListener listener) {
                 /* 
    P/P           *  Method: void removeChangeListener(CategoryChangeListener)
                  * 
                  *  Preconditions:
                  *    this.listeners != null
                  */
   342          listeners.remove(CategoryChangeListener.class, listener);
   343      }
   344      
   345      /**
   346       * Informs all registered listeners that this category has been selected.
   347       */
   348      public void fireCategorySelected() {
                 /* 
    P/P           *  Method: void fireCategorySelected()
                  * 
                  *  Preconditions:
                  *    this.listeners != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.util.ListenerList:get(...)@349 != null
                  *    java.util.Iterator:next(...)@349 != null
                  * 
                  *  Test Vectors:
                  *    java.util.Iterator:hasNext(...)@349: {0}, {1}
                  */
   349          for (CategoryChangeListener listener : listeners.get(CategoryChangeListener.class)) {
   350              listener.categorySelected(this);
   351          }
   352      }
   353      
   354      /**
   355       * Informs all registered listeners that this category has been deselected.
   356       */
   357      public void fireCategoryDeselected() {
                 /* 
    P/P           *  Method: void fireCategoryDeselected()
                  * 
                  *  Preconditions:
                  *    this.listeners != null
                  * 
                  *  Presumptions:
                  *    com.dmdirc.util.ListenerList:get(...)@358 != null
                  *    java.util.Iterator:next(...)@358 != null
                  * 
                  *  Test Vectors:
                  *    java.util.Iterator:hasNext(...)@358: {0}, {1}
                  */
   358          for (CategoryChangeListener listener : listeners.get(CategoryChangeListener.class)) {
   359              listener.categoryDeselected(this);
   360          }
   361      }    
   362  
   363  }








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