//
// Copyright 2011-2012 Jeff Bush
//
// Licensed under the Apache License, Version 2.0 (the "License");
// you may not use this file except in compliance with the License.
// You may obtain a copy of the License at
//
//     http://www.apache.org/licenses/LICENSE-2.0
//
// Unless required by applicable law or agreed to in writing, software
// distributed under the License is distributed on an "AS IS" BASIS,
// WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
// See the License for the specific language governing permissions and
// limitations under the License.
//

import java.util.*;
import java.io.*;

///
/// Converts a bitvector to a set of strings from an enumeration. Useful for
/// encoding state variables.
///

class EnumValueFormatter implements ValueFormatter {
    private class Mapping {
        Mapping(int _value, String _name) {
            value = _value;
            name = _name;
        }

        int value;
        String name;
    };

    EnumValueFormatter() {}

    void loadFromFile(File file) throws IOException {
        fFile = file;
        BufferedReader br = new BufferedReader(new InputStreamReader(new FileInputStream(file)));
        String line;
        while ((line = br.readLine()) != null) {
            String [] tokens = line.split(" ");
            if (tokens.length >= 2)
                fMappings.put(Integer.parseInt(tokens[0]), tokens[1]);
        }
    }

    File getFile() {
        return fFile;
    }

    @Override
    public String format(BitVector bits) {
        int mapIndex = bits.intValue();
        if (fMappings.containsKey(mapIndex))
            return fMappings.get(mapIndex);
        else
            return "??? (" + mapIndex + ")";
    }

    private HashMap<Integer, String> fMappings = new HashMap<Integer, String>();
    private File fFile;
}

@@ -662,16 +662,23 @@
 ctor to 
+one of 
 a set of
@@ -706,16 +706,20 @@
 eration.
+%0A///
  Useful 
@@ -721,20 +721,16 @@
 eful for
-%0A///
  encodin
@@ -810,222 +810,8 @@
 r %7B%0A
-    private class Mapping %7B%0A        Mapping(int _value, String _name) %7B%0A            value = _value;%0A            name = _name;%0A        %7D%0A%0A        int value;%0A        String name;%0A    %7D;%0A%0A    EnumValueFormatter() %7B%7D%0A%0A
     

Remove disused EnumValueFormatter.Mapping