// add all encodable characters
copy(encodable_.begin(), encodable_.end(), back_inserter(symbols));
// now the ones from the unicodesymbols file that are not already there
// add all encodable characters
copy(encodable_.begin(), encodable_.end(), back_inserter(symbols));
// now the ones from the unicodesymbols file that are not already there