@@ -76,27 +76,24 @@ public class JavaTextAreaPainter extends TextAreaPainter
7676 protected Font gutterTextFont;
7777 protected Color gutterTextColor;
7878 protected Color gutterLineHighlightColor;
79- // protected Color gutterTempColor;
8079
8180 public static class ErrorLineCoord {
82- public int xStart;
83- public int xEnd;
84- public int yStart;
85- public int yEnd;
86- public Problem problem;
87-
88- public ErrorLineCoord(int xStart, int xEnd, int yStart, int yEnd, Problem problem) {
89- this.xStart = xStart;
90- this.xEnd = xEnd;
91- this.yStart = yStart;
92- this.yEnd = yEnd;
93- this.problem = problem;
81+ public int xStart;
82+ public int xEnd;
83+ public int yStart;
84+ public int yEnd;
85+ public Problem problem;
86+
87+ public ErrorLineCoord(int xStart, int xEnd, int yStart, int yEnd, Problem problem) {
88+ this.xStart = xStart;
89+ this.xEnd = xEnd;
90+ this.yStart = yStart;
91+ this.yEnd = yEnd;
92+ this.problem = problem;
9493 }
9594 }
9695 public List<ErrorLineCoord> errorLineCoords = new ArrayList<>();
9796
98- // static int ctrlMask = Toolkit.getDefaultToolkit().getMenuShortcutKeyMask();
99-
10097
10198 public JavaTextAreaPainter(JavaTextArea textArea, TextAreaDefaults defaults) {
10299 super(textArea, defaults);
@@ -271,7 +268,10 @@ protected void paintLeftGutter(Graphics gfx, int line, int x) {
271268 }
272269 gfx.fillRect(0, y, Editor.LEFT_GUTTER, fm.getHeight());
273270
274- String text = getTextArea().getGutterText(line);
271+ String text = null;
272+ if (getEditor().isDebuggerEnabled()) {
273+ text = getTextArea().getGutterText(line);
274+ }
275275 // if no special text for a breakpoint, just show the line number
276276 if (text == null) {
277277 text = String.valueOf(line + 1);
@@ -293,6 +293,7 @@ protected void paintLeftGutter(Graphics gfx, int line, int x) {
293293 }
294294
295295
296+ /*
296297 // Failed attempt to switch line numbers to old-style figures
297298 String makeOSF(String what) {
298299 char[] c = what.toCharArray();
@@ -301,81 +302,7 @@ String makeOSF(String what) {
301302 }
302303 return new String(c);
303304 }
304-
305-
306- // /**
307- // * Paint the gutter background (solid color).
308- // *
309- // * @param gfx
310- // * the graphics context
311- // * @param line
312- // * 0-based line number
313- // * @param x
314- // * horizontal position
315- // */
316- // protected void paintGutterBg(Graphics gfx, int line, int x) {
317- // gfx.setColor(getTextArea().gutterBgColor);
318- // gfx.setColor(Color.ORANGE);
319- // int y = textArea.lineToY(line) + fm.getLeading() + fm.getMaxDescent();
320- // gfx.fillRect(0, y, Editor.LEFT_GUTTER, fm.getHeight());
321- // }
322-
323-
324- // /**
325- // * Paint the vertical gutter separator line.
326- // *
327- // * @param gfx
328- // * the graphics context
329- // * @param line
330- // * 0-based line number
331- // * @param x
332- // * horizontal position
333- // */
334- // protected void paintGutterLine(Graphics gfx, int line, int x) {
335- // int y = textArea.lineToY(line) + fm.getLeading() + fm.getMaxDescent();
336- // gfx.setColor(getTextArea().gutterLineColor);
337- // gfx.setColor(Color.GREEN);
338- // gfx.drawLine(Editor.LEFT_GUTTER, y,
339- // Editor.LEFT_GUTTER, y + fm.getHeight());
340- // }
341-
342-
343- // /**
344- // * Paint the gutter text.
345- // *
346- // * @param gfx
347- // * the graphics context
348- // * @param line
349- // * 0-based line number
350- // * @param x
351- // * horizontal position
352- // */
353- // protected void paintGutterText(Graphics gfx, int line, int x) {
354- // String text = getTextArea().getGutterText(line);
355- // if (text == null) {
356- // return;
357- // }
358- //
359- // gfx.setFont(getFont());
360- // Color textColor = getTextArea().getGutterTextColor(line);
361- // if (textColor == null) {
362- // gfx.setColor(getForeground());
363- // } else {
364- // gfx.setColor(textColor);
365- // }
366- // int y = textArea.lineToY(line) + fm.getHeight();
367- //
368- // // draw 4 times to make it appear bold, displaced 1px to the right, to the bottom and bottom right.
369- // //int len = text.length() > ta.gutterChars ? ta.gutterChars : text.length();
370- // Utilities.drawTabbedText(new Segment(text.toCharArray(), 0, text.length()),
371- // Editor.GUTTER_MARGIN, y, gfx, this, 0);
372- // Utilities.drawTabbedText(new Segment(text.toCharArray(), 0, text.length()),
373- // Editor.GUTTER_MARGIN + 1, y, gfx, this, 0);
374- // Utilities.drawTabbedText(new Segment(text.toCharArray(), 0, text.length()),
375- // Editor.GUTTER_MARGIN, y + 1, gfx, this, 0);
376- // Utilities.drawTabbedText(new Segment(text.toCharArray(), 0, text.length()),
377- // Editor.GUTTER_MARGIN + 1, y + 1, gfx, this, 0);
378- // }
305+ */
379306
380307
381308 /**
0 commit comments