misc notes and repair ConcurrentModificationException in the editor (fixes #3726)

This commit is contained in:
Ben Fry
2015-08-27 08:07:01 -04:00
parent 45ee8982ff
commit 5fd4dce6f4
5 changed files with 43 additions and 10 deletions

View File

@@ -2514,6 +2514,16 @@ public class JavaEditor extends Editor {
}
/*
public void clearErrorPoints() {
List<LineMarker> errorPoints = getErrorPoints();
synchronized (errorPoints) { // necessary?
errorPoints.clear();
}
}
*/
public void repaintErrorBar() {
errorColumn.repaint();
}

View File

@@ -996,8 +996,9 @@ public class ErrorCheckerService implements Runnable {
// editor.statusNotice("Position: " +
// editor.getTextArea().getCaretLine());
if (JavaMode.errorCheckEnabled) {
synchronized (editor.getErrorPoints()) {
for (LineMarker emarker : editor.getErrorPoints()) {
List<LineMarker> errorPoints = editor.getErrorPoints();
synchronized (errorPoints) {
for (LineMarker emarker : errorPoints) {
if (emarker.getProblem().getLineNumber() == editor.getTextArea().getCaretLine()) {
if (emarker.getType() == LineMarker.WARNING) {
editor.statusMessage(emarker.getProblem().getMessage(),
@@ -1590,6 +1591,7 @@ public class ErrorCheckerService implements Runnable {
public void handleErrorCheckingToggle() {
if (!JavaMode.errorCheckEnabled) {
Messages.log(editor.getSketch().getName() + " Error Checker paused.");
//editor.clearErrorPoints();
editor.getErrorPoints().clear();
problemsList.clear();
updateErrorTable();

View File

@@ -345,15 +345,18 @@ public class JavaTextAreaPainter extends TextAreaPainter
errorLineCoords.clear();
// Check if current line contains an error. If it does, find if it's an
// error or warning
for (LineMarker emarker : getJavaEditor().getErrorPoints()) {
if (emarker.getProblem().getLineNumber() == line) {
notFound = false;
if (emarker.getType() == LineMarker.WARNING) {
isWarning = true;
List<LineMarker> errorPoints = getJavaEditor().getErrorPoints();
synchronized (errorPoints) {
for (LineMarker emarker : errorPoints) {
if (emarker.getProblem().getLineNumber() == line) {
notFound = false;
if (emarker.getType() == LineMarker.WARNING) {
isWarning = true;
}
problem = emarker.getProblem();
//log(problem.toString());
break;
}
problem = emarker.getProblem();
//log(problem.toString());
break;
}
}