From 1b1e41b384581304a80ae136a6bbc29d3fb2b78f Mon Sep 17 00:00:00 2001 From: Dave Parker Date: Tue, 9 Mar 2021 10:03:02 +0000 Subject: [PATCH] Update PRISM editor to newer Swing drawing methods. Aiming to fix some issues on high DPI displays. Resolves #127. This is the first commit to master which requires Java >=9. --- .../userinterface/model/PepaEditorKit.java | 73 +++-------- .../userinterface/model/PrismEditorKit.java | 76 ++---------- .../model/pepaModel/GUIPepaModelEditor.java | 116 ++++++++---------- 3 files changed, 82 insertions(+), 183 deletions(-) diff --git a/prism/src/userinterface/model/PepaEditorKit.java b/prism/src/userinterface/model/PepaEditorKit.java index d25bec62..1a7d7f9f 100644 --- a/prism/src/userinterface/model/PepaEditorKit.java +++ b/prism/src/userinterface/model/PepaEditorKit.java @@ -124,7 +124,7 @@ class PepaContext extends StyleContext implements ViewFactory class PepaView extends PlainView { - static final userinterface.model.Style PLAIN_S = new userinterface.model.Style(Color.black, Font.PLAIN); + static final Style PLAIN_S = new Style(Color.black, Font.PLAIN); private Matcher match; private Pattern pattern; private GUIMultiModelHandler handler; @@ -136,107 +136,72 @@ class PepaView extends PlainView pattern = Pattern.compile("%.*"); } - protected int drawUnselectedText(Graphics g, int x, int y, int p0, int p1) throws BadLocationException + @Override + protected float drawUnselectedText(Graphics2D g, float x, float y, int p0, int p1) throws BadLocationException { int stLine = findStartOfLine(p0, getDocument()); int enLine = findEndOfLine(p1, getDocument()); - - if (g instanceof Graphics2D) { - Graphics2D g2d = (Graphics2D)g; - g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON); - } - + g.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON); try { g.setColor(Color.green); Document doc = getDocument(); - Segment segment = getLineBuffer(); - - - //String s = doc.getText(p0, p1-p0); String s = doc.getText(stLine, enLine-stLine); - userinterface.model.Style[] styles = highlight(s, (p0-stLine), (p1-p0)); - int currStart = 0; - int currEnd = 0; - Color last = null; + Style[] styles = highlight(s, (p0-stLine), (p1-p0)); String fname = handler.getPepaEditorFontFast().getName(); int fsize = handler.getPepaEditorFontFast().getSize(); - - for(int curr = 0; curr < styles.length; curr++) - { - - userinterface.model.Style c = styles[curr]; - + for (int curr = 0; curr < styles.length; curr++) { + Style c = styles[curr]; g.setColor(c.c); g.setFont(new Font(fname, c.style, fsize)); Segment segm = getLineBuffer(); doc.getText(p0+curr, 1, segm); x = Utilities.drawTabbedText(segm, x, y, g, this, p0+curr); - } g.setColor(Color.black); g.setFont(new Font(fname, Font.PLAIN, fsize)); } - catch(BadLocationException ex) - { + catch(BadLocationException ex) { //System.out.println("ex = "+ex); //ex.printStackTrace(); } return x; } - protected int drawSelectedText(Graphics g, int x, int y, int p0, int p1) throws BadLocationException + @Override + protected float drawSelectedText(Graphics2D g, float x, float y,int p0, int p1) throws BadLocationException { int stLine = findStartOfLine(p0, getDocument()); int enLine = findEndOfLine(p1, getDocument()); - - if (g instanceof Graphics2D) { - Graphics2D g2d = (Graphics2D)g; - g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON); - } - - try - { + g.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON); + try { g.setColor(Color.green); Document doc = getDocument(); - Segment segment = getLineBuffer(); - - - //String s = doc.getText(p0, p1-p0); String s = doc.getText(stLine, enLine-stLine); - userinterface.model.Style[] styles = highlight(s, (p0-stLine), (p1-p0)); - int currStart = 0; - int currEnd = 0; - Color last = null; + Style[] styles = highlight(s, (p0-stLine), (p1-p0)); String fname = handler.getPepaEditorFontFast().getName(); int fsize = handler.getPepaEditorFontFast().getSize(); - - for(int curr = 0; curr < styles.length; curr++) - { - - userinterface.model.Style c = styles[curr]; - + for (int curr = 0; curr < styles.length; curr++) { + Style c = styles[curr]; g.setColor(c.c); g.setFont(new Font(fname, c.style, fsize)); Segment segm = getLineBuffer(); doc.getText(p0+curr, 1, segm); x = Utilities.drawTabbedText(segm, x, y, g, this, p0+curr); - } g.setColor(Color.black); g.setFont(new Font(fname, Font.PLAIN, fsize)); } - catch(BadLocationException ex) - { + catch(BadLocationException ex) { //System.out.println("ex = "+ex); //ex.printStackTrace(); } return x; } - private synchronized userinterface.model.Style[] highlight(String s, int offset, int length) + private synchronized Style[] highlight(String s, int offset, int length) { - userinterface.model.Style[] styles = new userinterface.model.Style[s.length()]; + Style[] styles = new Style[s.length()]; for(int i = 0; i < styles.length; i++) styles[i] = PLAIN_S; @@ -261,7 +226,7 @@ class PepaView extends PlainView //System.out.println("styles.length = "+styles.length); //System.out.println("ret.length = "+length); //System.out.println("offset = "+offset); - userinterface.model.Style[]ret = new userinterface.model.Style[length]; + Style[]ret = new Style[length]; for(int i = 0; i < ret.length; i++) { ret[i] = styles[i+offset]; diff --git a/prism/src/userinterface/model/PrismEditorKit.java b/prism/src/userinterface/model/PrismEditorKit.java index 3bbbeaae..7032c999 100644 --- a/prism/src/userinterface/model/PrismEditorKit.java +++ b/prism/src/userinterface/model/PrismEditorKit.java @@ -32,7 +32,6 @@ package userinterface.model; import java.awt.Color; import java.awt.Font; -import java.awt.Graphics; import java.awt.Graphics2D; import java.awt.RenderingHints; @@ -139,113 +138,62 @@ class PrismView extends PlainView this.handler = handler; } - protected int drawUnselectedText(Graphics g, int x, int y,int p0, int p1) throws BadLocationException + @Override + protected float drawUnselectedText(Graphics2D g, float x, float y, int p0, int p1) throws BadLocationException { 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+"."); - try - { + g.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON); + try { g.setColor(Color.green); Document doc = getDocument(); - // Segment segment = getLineBuffer(); - - // System.out.println(doc.getText(p0, p1-p0)); - // String s = doc.getText(p0, p1-p0); String s = doc.getText(stLine, enLine-stLine); - // System.out.println("------"); - // System.out.println("highlighting unselected string = \n"+s); - // System.out.println("------"); - Style[] styles = highlight(s, (p0-stLine), (p1-p0)); - int currStart = 0; - int currEnd = 0; - Color last = null; String fname = handler.getPrismEditorFontFast().getName(); int fsize = handler.getPrismEditorFontFast().getSize(); - for(int curr = 0; curr < styles.length; curr++) - { - + for (int curr = 0; curr < styles.length; curr++) { Style c = styles[curr]; - g.setColor(c.c); g.setFont(new Font(fname, c.style, fsize)); Segment segm = new Segment();// getLineBuffer(); doc.getText(p0+curr, 1, segm); x = Utilities.drawTabbedText(segm, x, y, g, this, p0+curr); - } g.setColor(Color.black); g.setFont(new Font(fname, Font.PLAIN, fsize)); } - catch(BadLocationException ex) - { + catch(BadLocationException ex) { ex.printStackTrace(); } return x; } - protected int drawSelectedText(Graphics g, int x, int y,int p0, int p1) throws BadLocationException + @Override + protected float drawSelectedText(Graphics2D g, float x, float y,int p0, int p1) throws BadLocationException { 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+"."); - try - { + g.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON); + try { g.setColor(Color.green); Document doc = getDocument(); - // Segment segment = getLineBuffer(); - - - // String s = doc.getText(p0, p1-p0); - // System.out.println(doc.getText(p0, p1-p0)); - - String s = doc.getText(stLine, enLine-stLine); - // System.out.println("------"); - // System.out.println("highlighting selected string = \n"+s); - // System.out.println("------"); Style[] styles = highlight(s, (p0-stLine), (p1-p0)); - int currStart = 0; - int currEnd = 0; - Color last = null; String fname = handler.getPrismEditorFontFast().getName(); int fsize = handler.getPrismEditorFontFast().getSize(); - - for(int curr = 0; curr < styles.length; curr++) - { - + for (int curr = 0; curr < styles.length; curr++) { Style c = styles[curr]; - g.setColor(c.c); g.setFont(new Font(fname, c.style, fsize)); Segment segm = new Segment();// getLineBuffer(); doc.getText(p0+curr, 1, segm); x = Utilities.drawTabbedText(segm, x, y, g, this, p0+curr); - } g.setColor(Color.black); g.setFont(new Font(fname, Font.PLAIN, fsize)); } - catch(BadLocationException ex) - { + catch(BadLocationException ex) { ex.printStackTrace(); } return x; diff --git a/prism/src/userinterface/model/pepaModel/GUIPepaModelEditor.java b/prism/src/userinterface/model/pepaModel/GUIPepaModelEditor.java index 274ebd1f..a09acd98 100644 --- a/prism/src/userinterface/model/pepaModel/GUIPepaModelEditor.java +++ b/prism/src/userinterface/model/pepaModel/GUIPepaModelEditor.java @@ -27,18 +27,41 @@ package userinterface.model.pepaModel; -import javax.swing.*; -import javax.swing.text.*; +import java.awt.BorderLayout; +import java.awt.Color; +import java.awt.Font; +import java.awt.Graphics; +import java.awt.Graphics2D; +import java.awt.RenderingHints; +import java.awt.Shape; +import java.io.IOException; +import java.io.Reader; +import java.io.Writer; +import java.util.regex.Matcher; +import java.util.regex.Pattern; + +import javax.swing.JEditorPane; +import javax.swing.JScrollPane; +import javax.swing.event.DocumentEvent; +import javax.swing.event.DocumentListener; +import javax.swing.text.BadLocationException; +import javax.swing.text.DefaultEditorKit; +import javax.swing.text.Document; +import javax.swing.text.Element; +import javax.swing.text.PlainDocument; +import javax.swing.text.PlainView; +import javax.swing.text.Segment; +import javax.swing.text.StyleContext; +import javax.swing.text.Utilities; +import javax.swing.text.View; +import javax.swing.text.ViewFactory; import javax.swing.undo.CannotRedoException; import javax.swing.undo.CannotUndoException; import javax.swing.undo.UndoManager; -import java.util.regex.*; -import java.awt.*; - -import javax.swing.event.*; -import java.io.*; -import userinterface.model.*; +import userinterface.model.GUIModelEditor; +import userinterface.model.GUIMultiModelHandler; +import userinterface.model.Style; public class GUIPepaModelEditor extends GUIModelEditor implements DocumentListener { @@ -235,7 +258,7 @@ public class GUIPepaModelEditor extends GUIModelEditor implements DocumentListen } - static final userinterface.model.Style PLAIN_S = new userinterface.model.Style(Color.black, Font.PLAIN); + static final Style PLAIN_S = new Style(Color.black, Font.PLAIN); class PepaView extends PlainView { @@ -253,108 +276,71 @@ public class GUIPepaModelEditor extends GUIModelEditor implements DocumentListen super.paint(g, a); } - - protected int drawUnselectedText(Graphics g, int x, int y,int p0, int p1) throws BadLocationException + @Override + protected float drawUnselectedText(Graphics2D g, float x, float y, int p0, int p1) throws BadLocationException { int stLine = findStartOfLine(p0, getDocument()); int enLine = findEndOfLine(p1, getDocument()); - - if (g instanceof Graphics2D) { - Graphics2D g2d = (Graphics2D)g; - g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON); - } - - try - { + g.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON); + try { g.setColor(Color.green); Document doc = getDocument(); - Segment segment = getLineBuffer(); - - - //String s = doc.getText(p0, p1-p0); String s = doc.getText(stLine, enLine-stLine); - userinterface.model.Style[] styles = highlight(s, (p0-stLine), (p1-p0)); - int currStart = 0; - int currEnd = 0; - Color last = null; + Style[] styles = highlight(s, (p0-stLine), (p1-p0)); String fname = handler.getPepaEditorFontFast().getName(); int fsize = handler.getPepaEditorFontFast().getSize(); - - for(int curr = 0; curr < styles.length; curr++) - { - - userinterface.model.Style c = styles[curr]; - + for (int curr = 0; curr < styles.length; curr++) { + Style c = styles[curr]; g.setColor(c.c); g.setFont(new Font(fname, c.style, fsize)); Segment segm = getLineBuffer(); doc.getText(p0+curr, 1, segm); x = Utilities.drawTabbedText(segm, x, y, g, this, p0+curr); - } g.setColor(Color.black); g.setFont(new Font(fname, Font.PLAIN, fsize)); } - catch(BadLocationException ex) - { + catch(BadLocationException ex) { //System.out.println("ex = "+ex); //ex.printStackTrace(); } return x; } - protected int drawSelectedText(Graphics g, int x, int y,int p0, int p1) throws BadLocationException + @Override + protected float drawSelectedText(Graphics2D g, float x, float y,int p0, int p1) throws BadLocationException { int stLine = findStartOfLine(p0, getDocument()); int enLine = findEndOfLine(p1, getDocument()); - - if (g instanceof Graphics2D) { - Graphics2D g2d = (Graphics2D)g; - g2d.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON); - } - - try - { + g.setRenderingHint(RenderingHints.KEY_TEXT_ANTIALIASING, RenderingHints.VALUE_TEXT_ANTIALIAS_ON); + try { g.setColor(Color.green); Document doc = getDocument(); - Segment segment = getLineBuffer(); - - - //String s = doc.getText(p0, p1-p0); String s = doc.getText(stLine, enLine-stLine); - userinterface.model.Style[] styles = highlight(s, (p0-stLine), (p1-p0)); - int currStart = 0; - int currEnd = 0; - Color last = null; + Style[] styles = highlight(s, (p0-stLine), (p1-p0)); String fname = handler.getPepaEditorFontFast().getName(); int fsize = handler.getPepaEditorFontFast().getSize(); - - for(int curr = 0; curr < styles.length; curr++) - { - - userinterface.model.Style c = styles[curr]; - + for(int curr = 0; curr < styles.length; curr++) { + Style c = styles[curr]; g.setColor(c.c); g.setFont(new Font(fname, c.style, fsize)); Segment segm = getLineBuffer(); doc.getText(p0+curr, 1, segm); x = Utilities.drawTabbedText(segm, x, y, g, this, p0+curr); - } g.setColor(Color.black); g.setFont(new Font(fname, Font.PLAIN, fsize)); } - catch(BadLocationException ex) - { + catch(BadLocationException ex) { //System.out.println("ex = "+ex); //ex.printStackTrace(); } return x; } - private synchronized userinterface.model.Style[] highlight(String s, int offset, int length) + private synchronized Style[] highlight(String s, int offset, int length) { - userinterface.model.Style[] styles = new userinterface.model.Style[s.length()]; + Style[] styles = new Style[s.length()]; for(int i = 0; i < styles.length; i++) styles[i] = PLAIN_S; @@ -379,7 +365,7 @@ public class GUIPepaModelEditor extends GUIModelEditor implements DocumentListen //System.out.println("styles.length = "+styles.length); //System.out.println("ret.length = "+length); //System.out.println("offset = "+offset); - userinterface.model.Style[]ret = new userinterface.model.Style[length]; + Style[]ret = new Style[length]; for(int i = 0; i < ret.length; i++) { ret[i] = styles[i+offset];