(cm)
| 30 | } |
| 31 | |
| 32 | function setNormal(cm) { |
| 33 | var wrap = cm.getWrapperElement(); |
| 34 | wrap.className = wrap.className.replace(/\s*CodeMirror-fullscreen\b/, ""); |
| 35 | document.documentElement.style.overflow = ""; |
| 36 | var info = cm.state.fullScreenRestore; |
| 37 | wrap.style.width = info.width; wrap.style.height = info.height; |
| 38 | window.scrollTo(info.scrollLeft, info.scrollTop); |
| 39 | cm.refresh(); |
| 40 | } |
| 41 | }); |