001 /* 002 * This file is part of the Jikes RVM project (http://jikesrvm.org). 003 * 004 * This file is licensed to You under the Eclipse Public License (EPL); 005 * You may not use this file except in compliance with the License. You 006 * may obtain a copy of the License at 007 * 008 * http://www.opensource.org/licenses/eclipse-1.0.php 009 * 010 * See the COPYRIGHT.txt file distributed with this work for information 011 * regarding copyright ownership. 012 */ 013 package org.vmutil.options; 014 015 import org.vmmagic.pragma.Uninterruptible; 016 017 /** 018 * An option with a simple integer value. 019 */ 020 public class IntOption extends Option { 021 // values 022 protected int defaultValue; 023 protected int value; 024 025 /** 026 * Create a new int option. 027 * 028 * @param set The option set this option belongs to. 029 * @param name The space separated name for the option. 030 * @param desc The purpose of the option 031 * @param defaultValue The default value of the option. 032 */ 033 protected IntOption(OptionSet set, String name, String desc, int defaultValue) { 034 super(set, INT_OPTION, name, desc); 035 this.value = this.defaultValue = defaultValue; 036 } 037 038 /** 039 * Read the current value of the option. 040 * 041 * @return The option value. 042 */ 043 @Uninterruptible 044 public int getValue() { 045 return this.value; 046 } 047 048 /** 049 * Read the default value of the option. 050 * 051 * @return The default value. 052 */ 053 @Uninterruptible 054 public int getDefaultValue() { 055 return this.defaultValue; 056 } 057 058 /** 059 * Update the value of the option, echoing the change if the echoOptions 060 * option is set. This method also calls the validate method to allow 061 * subclasses to perform any required validation. 062 * 063 * @param value The new value for the option. 064 */ 065 public void setValue(int value) { 066 this.value = value; 067 validate(); 068 set.logChange(this); 069 } 070 071 /** 072 * Modify the default value of the option. 073 * 074 * @param value The new default value for the option. 075 */ 076 public void setDefaultValue(int value) { 077 this.value = this.defaultValue = value; 078 } 079 }