()
| 1354 | startWorker(); |
| 1355 | } |
| 1356 | function gutterChanged() { |
| 1357 | var visible = options.gutter || options.lineNumbers; |
| 1358 | gutter.style.display = visible ? "" : "none"; |
| 1359 | if (visible) gutterDirty = true; |
| 1360 | else lineDiv.parentNode.style.marginLeft = 0; |
| 1361 | } |
| 1362 | function wrappingChanged(from, to) { |
| 1363 | if (options.lineWrapping) { |
| 1364 | wrapper.className += " CodeMirror-wrap"; |