- /** this method invokes the platform _createSurface() method and then enforces a few post-call invariants */
- public static Surface createSurface(Box b, boolean framed, boolean refreshable) {
- Surface ret = platform._createSurface(b, framed);
- ret.setInvisible(b.invisible);
- b.set(Box.size, 0, ret.width);
- b.set(Box.size, 1, ret.height);
-
- Object titlebar = b.get("titlebar", null, true);
- if (titlebar != null) ret.setTitleBarText(titlebar.toString());
-
- Object icon = b.get("icon", null, true);
- if (icon != null && !"".equals(icon)) {
- Picture pic = Box.getPicture(icon.toString());
- if (pic != null) ret.setIcon(pic);
- else if (Log.on) Log.log(Platform.class, "unable to load icon " + icon);
- }
-
- if (refreshable) {
- Surface.refreshableSurfaceWasCreated = true;
- Surface.allSurfaces.addElement(ret);
- ret.dirty(0, 0, ret.width, ret.height);
- ret.Refresh();
- }
- return ret;
- }
-
- // Helpful font parsing stuff //////////////////////////////////////////////////////
-
- public static class ParsedFont {
- public ParsedFont() { }
- public ParsedFont(String s) { parse(s); }
- public int size = 10;
- public String name = "";
-
- public boolean italic = false;
- public boolean bold = false;
- public boolean underline = false;
- public boolean dotted_underline = false;
-
- private static int stoi(Object o) {
- if (o == null) return 0;
- if (o instanceof Integer) return ((Integer)o).intValue();
-
- String s = o.toString();
- try { return Integer.parseInt(s.indexOf('.') == -1 ? s : s.substring(0, s.indexOf('.'))); }
- catch (NumberFormatException e) { return 0; }
- }
-
- public void parse(String font) {
- int i = 0;
- while(i < font.length() && !Character.isDigit(font.charAt(i))) i++;
- name = font.substring(0, i).toLowerCase().replace('_', ' ');
- size = 10;
- italic = false;
- bold = false;
- underline = false;
- dotted_underline = false;
- if (i != font.length()) {
- int j = i;
- while (j < font.length() && Character.isDigit(font.charAt(j))) j++;
- if (i != j) size = stoi(font.substring(i, j));
- i = j;
- while(i < font.length()) {
- switch (font.charAt(i)) {
- case 'b': bold = true;
- case 'i': italic = true;
- case 'd': dotted_underline = true;
- case 'u': underline = true;
- }
- i++;
- }
+ /** detects proxy settings */
+ protected synchronized org.xwt.HTTP.Proxy _detectProxy() { return null; }
+ public static synchronized org.xwt.HTTP.Proxy detectProxy() {
+
+ if (cachedProxyInfo != null) return cachedProxyInfo;
+ if (alreadyDetectedProxy) return null;
+ alreadyDetectedProxy = true;
+
+ if (Log.on) Log.info(Platform.class, "attempting environment-variable DNS proxy detection");
+ cachedProxyInfo = org.xwt.HTTP.Proxy.detectProxyViaManual();
+ if (cachedProxyInfo != null) return cachedProxyInfo;
+
+ if (Log.on) Log.info(Platform.class, "attempting " + platform.getClass().getName() + " proxy detection");
+ cachedProxyInfo = platform._detectProxy();
+ if (cachedProxyInfo != null) return cachedProxyInfo;
+
+ return cachedProxyInfo;
+ }
+
+ /** returns a Scheduler instance; used to implement platform-specific schedulers */
+ protected Scheduler _getScheduler() { return new Scheduler(); }
+ public static Scheduler getScheduler() { return platform._getScheduler(); }
+
+ // FEATURE: be more efficient for many of the subclasses
+ public static class DefaultGlyph extends Font.Glyph {
+ private Picture p = null;
+ public DefaultGlyph(org.xwt.Font f, char c) { super(f, c); }
+ public Picture getPicture() {
+ if (p == null && isLoaded) {
+ p = createPicture(null);
+ p.data = new int[data.length];
+ for(int i=0; i<data.length; i++) p.data[i] = (data[i] & 0xff) << 24;
+ data = null;
+ p.width = this.width;
+ p.height = this.height;