Mercurial Mercurial > repos > isabelle / annotate
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Tools/jEdit/patches/cobra-0.98.4/create_font
author wenzelm
Sun, 20 May 2012 11:34:33 +0200
changeset 47884 21c42b095c84
parent 46816 a96b25141220
permissions -rw-r--r--
try to avoid races again (cf. 8c37cb84065f and fd3a36e48b09);
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
45911
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
     1
 
diff -ru cobra-0.98.4/src/org/lobobrowser/util/gui/FontFactory.java cobra-0.98.4-patched/src/org/lobobrowser/util/gui/FontFactory.java
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
     2
 
--- cobra-0.98.4/src/org/lobobrowser/util/gui/FontFactory.java	2008-12-28 17:33:38.000000000 +0100
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
     3
 
+++ cobra-0.98.4-patched/src/org/lobobrowser/util/gui/FontFactory.java	2011-12-17 15:57:03.000000000 +0100
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
     4
 
@@ -29,8 +29,6 @@
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
     5
 
 import java.util.logging.*;
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
     6
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
     7
 
 import org.lobobrowser.util.Objects;
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
     8
 
-/** Note: Undocumented class? */
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
     9
 
-import sun.font.FontManager;
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
    10
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
    11
 
 /**
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
    12
 
  * @author J. H. S.
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
    13
 
@@ -206,8 +204,7 @@
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
    14
 
 	}
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
    15
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
    16
 
 	private Font createFont(String name, int style, int size) {
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
    17
 
-		// Proprietary Sun API. Maybe shouldn't use it. Works well for Chinese.
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
    18
 
-	    return FontManager.getCompositeFontUIResource(new Font(name, style, size));
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
    19
 
+	    return new javax.swing.plaf.FontUIResource(name, style, size);
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
    20
 
 	}
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
    21
760895d5a600 patch for Lobo/Cobra 0.98.4 to make it work with Java 1.7 (see also http://sourceforge.net/tracker/index.php?func=detail&aid=2991043&group_id=139023&atid=742262);
wenzelm
parents:
diff changeset 
    22
 
 	private static class FontKey {
isabelle