155 |
155 |
156 public int size() { |
156 public int size() { |
157 return values.size(); |
157 return values.size(); |
158 } |
158 } |
159 |
159 |
|
160 // light-weight notification mechanism |
|
161 |
|
162 private List<Runnable> listeners = List.nil(); |
|
163 |
|
164 public void addListener(Runnable listener) { |
|
165 listeners = listeners.prepend(listener); |
|
166 } |
|
167 |
|
168 public void notifyListeners() { |
|
169 for (Runnable r: listeners) |
|
170 r.run(); |
|
171 } |
|
172 |
160 /** Check for a lint suboption. */ |
173 /** Check for a lint suboption. */ |
161 public boolean lint(String s) { |
174 public boolean lint(String s) { |
162 // return true if either the specific option is enabled, or |
175 // return true if either the specific option is enabled, or |
163 // they are all enabled without the specific one being |
176 // they are all enabled without the specific one being |
164 // disabled |
177 // disabled |