diff --git a/edit.js b/edit.js index 5eaa6fc3..bdf26d82 100644 --- a/edit.js +++ b/edit.js @@ -161,7 +161,8 @@ function initCodeMirror() { foldGutter: true, gutters: ["CodeMirror-linenumbers", "CodeMirror-foldgutter", "CodeMirror-lint-markers"], matchBrackets: true, - lint: CodeMirror.lint.css, + lint: {getAnnotations: CodeMirror.lint.css, delay: prefs.getPref("editor.lintDelay")}, + lintReportDelay: prefs.getPref("editor.lintReportDelay"), styleActiveLine: true, theme: "default", keyMap: prefs.getPref("editor.keyMap"), @@ -784,16 +785,28 @@ function updateLintReport(cm, delay) { lintOpt.delay = 1; return; } + // user is editing right now: postpone updating the report for the new issues (default: 500ms lint + 4500ms) + // or update it as soon as possible (default: 500ms lint + 100ms) in case an existing issue was just fixed + var postponeNewIssues = delay == undefined; var state = cm.state.lint; clearTimeout(state.reportTimeout); - state.reportTimeout = setTimeout(update.bind(cm), (state.options.delay || 500) + 4500); + state.reportTimeout = setTimeout(update.bind(cm), state.options.delay + 100); + function update() { // this == cm var scope = this ? [this] : editors; var changed = false; + var fixedOldIssues = false; scope.forEach(function(cm) { + var oldMarkers = cm.state.lint.markedLast || {}; + var newMarkers = {}; var html = cm.state.lint.marked.length == 0 ? "" : "
" + cm.state.lint.marked.map(function(mark) { var info = mark.__annotation; + var pos = info.from.line + "," + info.from.ch; + if (oldMarkers[pos] == info.message) { + delete oldMarkers[pos]; + } + newMarkers[pos] = info.message; return "