else if (name.equals("xmlrpc")) return xmlrpc;
else if (name.equals("clipboard")) return Platform.getClipBoard();
else if (name.equals("altKeyName")) return Platform.altKeyName();
+ else if (name.equals("screenWidth")) return new Integer(Platform.getScreenWidth());
+ else if (name.equals("screenHeight")) return new Integer(Platform.getScreenHeight());
else if (name.equals("static")) return Static.getStatic("");
else if (name.equals("theme")) return theme;
else if (name.equals("button")) {