Added anti-aliasing by default to model text editors.

Note that PepaEditorKit is changed here, but never used it seems.


git-svn-id: https://www.prismmodelchecker.org/svn/prism/prism/trunk@3299 bbc10eb1-c90d-0410-af57-cb519fbb1720

prism/src/userinterface/model/PepaEditorKit.java

@@ -32,6 +32,8 @@ package userinterface.model;
 import java.awt.Color;
 import java.awt.Font;
 import java.awt.Graphics;
+import java.awt.Graphics2D;
+import java.awt.RenderingHints;
 import java.util.regex.Matcher;
 import java.util.regex.Pattern;
 
@@ -138,7 +140,12 @@ class PepaView extends PlainView
 	{
 		int stLine = findStartOfLine(p0, getDocument());
 		int enLine = findEndOfLine(p1, getDocument());
-		//System.out.println("p0 = "+p0+", p1 = "+p1+", st = "+stLine+", enLine = "+enLine+".");
+
+		if (g instanceof Graphics2D) {
+			Graphics2D g2d = (Graphics2D)g;
+			g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
+		}
+        
 		try
 		{
 			g.setColor(Color.green);
@@ -182,7 +189,12 @@ class PepaView extends PlainView
 	{
 		int stLine = findStartOfLine(p0, getDocument());
 		int enLine = findEndOfLine(p1, getDocument());
-		//System.out.println("p0 = "+p0+", p1 = "+p1+", st = "+stLine+", enLine = "+enLine+".");
+
+		if (g instanceof Graphics2D) {
+			Graphics2D g2d = (Graphics2D)g;
+			g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
+		}
+        
 		try
 		{
 			g.setColor(Color.green);

prism/src/userinterface/model/PrismEditorKit.java

@@ -33,6 +33,8 @@ package userinterface.model;
 import java.awt.Color;
 import java.awt.Font;
 import java.awt.Graphics;
+import java.awt.Graphics2D;
+import java.awt.RenderingHints;
 
 import javax.swing.text.BadLocationException;
 import javax.swing.text.DefaultEditorKit;
@@ -142,6 +144,11 @@ class PrismView extends PlainView
 		int stLine = p0;// findStartOfLine(p0, getDocument());
 		int enLine = p1;// findEndOfLine(p1-1, getDocument());
 
+		if (g instanceof Graphics2D) {
+			Graphics2D g2d = (Graphics2D)g;
+			g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
+		}
+        
 		// x+= getLeftInset();
 		// System.out.println("p0 = "+p0+", p1 = "+p1+", st = "+stLine+",
 		// enLine = "+enLine+".");
@@ -192,6 +199,11 @@ class PrismView extends PlainView
 		int stLine = p0;// findStartOfLine(p0, getDocument());
 		int enLine = p1;// findEndOfLine(p1-1, getDocument());
 
+		if (g instanceof Graphics2D) {
+			Graphics2D g2d = (Graphics2D)g;
+			g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
+		}
+        
 		// x+= getLeftInset();
 		// System.out.println("p0 = "+p0+", p1 = "+p1+", st = "+stLine+",
 		// enLine = "+enLine+".");

prism/src/userinterface/model/pepaModel/GUIPepaModelEditor.java

@@ -35,6 +35,7 @@ import javax.swing.undo.UndoManager;
 
 import java.util.regex.*;
 import java.awt.*;
+
 import javax.swing.event.*;
 import java.io.*;
 import userinterface.model.*;
@@ -257,7 +258,12 @@ public class GUIPepaModelEditor extends GUIModelEditor implements DocumentListen
 		{
 			int stLine = findStartOfLine(p0, getDocument());
 			int enLine = findEndOfLine(p1, getDocument());
-			//System.out.println("p0 = "+p0+", p1 = "+p1+", st = "+stLine+", enLine = "+enLine+".");
+			
+			if (g instanceof Graphics2D) {
+				Graphics2D g2d = (Graphics2D)g;
+				g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
+			}
+	        
 			try
 			{
 				g.setColor(Color.green);
@@ -301,7 +307,12 @@ public class GUIPepaModelEditor extends GUIModelEditor implements DocumentListen
 		{
 			int stLine = findStartOfLine(p0, getDocument());
 			int enLine = findEndOfLine(p1, getDocument());
-			//System.out.println("p0 = "+p0+", p1 = "+p1+", st = "+stLine+", enLine = "+enLine+".");
+			
+			if (g instanceof Graphics2D) {
+				Graphics2D g2d = (Graphics2D)g;
+				g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON);
+			}
+	        
 			try
 			{
 				g.setColor(Color.green);