"Preferences" = "Preferences";
"Window" = "Window";
"Session" = "Session";
"Cols:" = "Cols:";
"Rows:" = "Rows:";
"Font" = "Font";
"Non-ASCII Font" = "Non-ASCII Font";
"Anti-Aliasing" = "Anti-Aliasing";
"Cancel" = "Cancel";
"OK" = "OK";
"Name:" = "Name:";
"Encoding:" = "Encoding:";
"Transparency:" = "Transparency:";
"Text:" = "Text:";
"Selection:" = "Selection:";
"Background:" = "Background:";
"Bold:" = "Bold:";
"Idle character" = "Idle character";
"ASCII code:" = "ASCII code:";