Function clearPlaceholder

external/.scrollLibs.js:13325–13330

(cm)

  })

  function clearPlaceholder(cm) {
    if (cm.state.placeholder) {
      cm.state.placeholder.parentNode.removeChild(cm.state.placeholder)
      cm.state.placeholder = null
    }
  }
  function setPlaceholder(cm) {
    clearPlaceholder(cm)
    var elt = (cm.state.placeholder = document.createElement("pre"))