0) { $value = db_fetch_result($result, 0, "value"); $type_name = db_fetch_result($result, 0, "type_name"); if ($user_id = $_SESSION["uid"]) { $_SESSION["prefs_cache"][$pref_name]["type"] = $type_name; $_SESSION["prefs_cache"][$pref_name]["value"] = $value; } return convert_pref_type($value, $type_name); } else { die("Fatal error, unknown preferences key: $pref_name"); } } function convert_pref_type($value, $type_name) { if ($type_name == "bool") { return $value == "true"; } else if ($type_name == "integer") { return sprintf("%d", $value); } else { return $value; } } ?>