()
| 1554 | startWorker(); |
| 1555 | } |
| 1556 | function gutterChanged() { |
| 1557 | var visible = options.gutter || options.lineNumbers; |
| 1558 | gutter.style.display = visible ? "" : "none"; |
| 1559 | if (visible) gutterDirty = true; |
| 1560 | else lineDiv.parentNode.style.marginLeft = 0; |
| 1561 | } |
| 1562 | function wrappingChanged(from, to) { |
| 1563 | if (options.lineWrapping) { |
| 1564 | wrapper.className += " CodeMirror-wrap"; |