View Javadoc

1   /********************************************************************************
2    *
3    *	Copyright (C) 2008 Fujitsu Services Ltd.
4    *
5    *	Author: Nick Battle
6    *
7    *	This file is part of VDMJ.
8    *	
9    *	VDMJ is free software: you can redistribute it and/or modify
10   *	it under the terms of the GNU General Public License as published by
11   *	the Free Software Foundation, either version 3 of the License, or
12   *	(at your option) any later version.
13   *	
14   *	VDMJ is distributed in the hope that it will be useful,
15   *	but WITHOUT ANY WARRANTY; without even the implied warranty of
16   *	MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
17   *	GNU General Public License for more details.
18   *	
19   *	You should have received a copy of the GNU General Public License
20   *	along with VDMJ.  If not, see <http://www.gnu.org/licenses/>.
21   *
22   ******************************************************************************/
23  
24  package org.overturetool.vdmj.values;
25  
26  import java.util.Vector;
27  
28  import org.overturetool.vdmj.lex.LexNameToken;
29  import org.overturetool.vdmj.util.Utils;
30  
31  
32  @SuppressWarnings("serial")
33  public class NameValuePairList extends Vector<NameValuePair>
34  {
35  	public NameValuePairList()
36  	{
37  		super();
38  	}
39  
40  	public NameValuePairList(NameValuePair nv)
41  	{
42  		add(nv);
43  	}
44  
45  	public boolean add(LexNameToken name, Value value)
46  	{
47  		return super.add(new NameValuePair(name, value));
48  	}
49  
50  	@Override
51  	public boolean add(NameValuePair nv)
52  	{
53  		return super.add(nv);
54  	}
55  
56  	public NameValuePairList getUpdatable(ValueListener listener)
57  	{
58  		NameValuePairList nlist = new NameValuePairList();
59  
60  		for (NameValuePair nvp: this)
61  		{
62  			nlist.add(nvp.name, nvp.value.getUpdatable(listener));
63  		}
64  
65  		return nlist;
66  	}
67  
68  	@Override
69  	public String toString()
70  	{
71  		return Utils.listToString("[", this, ", ", "]");
72  	}
73  }