|
|
@ -132,6 +132,8 @@ var executionMark; |
|
|
|
highlightExecution = function(start, end) { |
|
|
|
if (executionMark) |
|
|
|
executionMark.clear(); |
|
|
|
if (start === 0 && end + 1 === editor.getValue().length) |
|
|
|
return; // Do not hightlight the whole document.
|
|
|
|
executionMark = editor.markText(editor.posFromIndex(start), editor.posFromIndex(end), { className: "CodeMirror-exechighlight" }); |
|
|
|
} |
|
|
|
|
|
|
|