# HG changeset patch
# User wenzelm
# Date 1324135282 -3600
# Node ID 760895d5a600b4fad9de59dbf13d55239db50661
# Parent  566c34b64f7068326024172fd1dec94163e7ad87
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);

diff -r 566c34b64f70 -r 760895d5a600 src/Tools/jEdit/patches/cobra
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Tools/jEdit/patches/cobra	Sat Dec 17 16:21:22 2011 +0100
@@ -0,0 +1,22 @@
+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
+--- cobra-0.98.4/src/org/lobobrowser/util/gui/FontFactory.java	2008-12-28 17:33:38.000000000 +0100
++++ cobra-0.98.4-patched/src/org/lobobrowser/util/gui/FontFactory.java	2011-12-17 15:57:03.000000000 +0100
+@@ -29,8 +29,6 @@
+ import java.util.logging.*;
+ 
+ import org.lobobrowser.util.Objects;
+-/** Note: Undocumented class? */
+-import sun.font.FontManager;
+ 
+ /**
+  * @author J. H. S.
+@@ -206,8 +204,7 @@
+ 	}
+ 	
+ 	private Font createFont(String name, int style, int size) {
+-		// Proprietary Sun API. Maybe shouldn't use it. Works well for Chinese.
+-	    return FontManager.getCompositeFontUIResource(new Font(name, style, size));
++	    return new javax.swing.plaf.FontUIResource(name, style, size);
+ 	}
+ 	
+ 	private static class FontKey {