:	\n"; for ($i = 0; $i < count($theme); $i++) { if ($theme[$i]["PATH"] == $chosen_theme) echo " ".$theme[$i]["NAME"]."\n"; else echo " ".$theme[$i]["NAME"]."\n"; } echo " "; ?>
:	\n"; reset ($languages); while (list($code, $name)=each($languages)) { if ($code==$chosen_language) echo " ".$languages[$code]["NAME"]."\n"; else echo " ".$languages[$code]["NAME"]."\n"; } echo " "; ?>
	"; if ($use_javascript_addr_book == true) { echo " " . _("JavaScript") . "    "; echo " " . _("HTML"); } else { echo " " . _("JavaScript") . "    "; echo " " . _("HTML"); } ?>
:	"; else echo " "; ?>
:	"; else echo " "; ?>
:	= 10 && $editor_size <= 255) echo " "; else echo " "; ?>
:	\n"; if ($left_size == 100) echo "100 pixels\n"; else echo "100 pixels\n"; if ($left_size == 125) echo "125 pixels\n"; else echo "125 pixels\n"; if ($left_size == 150) echo "150 pixels\n"; else echo "150 pixels\n"; if ($left_size == 175) echo "175 pixels\n"; else echo "175 pixels\n"; if (($left_size == 200) || ($left_size == "")) echo "200 pixels\n"; else echo "200 pixels\n"; if (($left_size == 225)) echo "225 pixels\n"; else echo "225 pixels\n"; if (($left_size == 250)) echo "250 pixels\n"; else echo "250 pixels\n"; if ($left_size == 275) echo "275 pixels\n"; else echo "275 pixels\n"; if (($left_size == 300)) echo "300 pixels\n"; else echo "300 pixels\n"; echo " "; ?>
:	"; if (($left_refresh == "None") || ($left_refresh == "")) echo " None"; else echo " None"; if (($left_refresh == "10")) echo " 10 Seconds"; else echo " 10 Seconds"; if (($left_refresh == "20")) echo " 20 Seconds"; else echo " 20 Seconds"; if (($left_refresh == "30")) echo " 30 Seconds"; else echo " 30 Seconds"; if (($left_refresh == "60")) echo " 1 Minute"; else echo " 1 Minute"; if (($left_refresh == "120")) echo " 2 Minutes"; else echo " 2 Minutes"; if (($left_refresh == "180")) echo " 3 Minutes"; else echo " 3 Minutes"; if (($left_refresh == "240")) echo " 4 Minutes"; else echo " 4 Minutes"; if (($left_refresh == "300")) echo " 5 Minutes"; else echo " 5 Minutes"; if (($left_refresh == "420")) echo " 7 Minutes"; else echo " 7 Minutes"; if (($left_refresh == "600")) echo " 10 Minutes"; else echo " 10 Minutes"; if (($left_refresh == "720")) echo " 12 Minutes"; else echo " 12 Minutes"; if (($left_refresh == "900")) echo " 15 Minutes"; else echo " 15 Minutes"; if (($left_refresh == "1200")) echo " 20 Minutes"; else echo " 20 Minutes"; if (($left_refresh == "1500")) echo " 25 Minutes"; else echo " 25 Minutes"; if (($left_refresh == "1800")) echo " 30 Minutes"; else echo " 30 Minutes"; echo " "; ?>