diff options
| -rw-r--r-- | index.html | 1 | ||||
| -rw-r--r-- | js/codemirror/panel.js | 112 |
2 files changed, 0 insertions, 113 deletions
@@ -457,7 +457,6 @@ <!-- CodeMirror stuff --> <script src="js/codemirror/codemirror.js"></script> <script src="js/codemirror/matchbrackets.js"></script> - <script src="js/codemirror/panel.js"></script> <script src="js/codemirror/prolog.js"></script> <script src="js/codemirror/python.js"></script> <script src="js/codemirror/show-hint.js"></script> diff --git a/js/codemirror/panel.js b/js/codemirror/panel.js deleted file mode 100644 index ba29484..0000000 --- a/js/codemirror/panel.js +++ /dev/null @@ -1,112 +0,0 @@ -// CodeMirror, copyright (c) by Marijn Haverbeke and others -// Distributed under an MIT license: http://codemirror.net/LICENSE - -(function(mod) { - if (typeof exports == "object" && typeof module == "object") // CommonJS - mod(require("../../lib/codemirror")); - else if (typeof define == "function" && define.amd) // AMD - define(["../../lib/codemirror"], mod); - else // Plain browser env - mod(CodeMirror); -})(function(CodeMirror) { - CodeMirror.defineExtension("addPanel", function(node, options) { - options = options || {}; - - if (!this.state.panels) initPanels(this); - - var info = this.state.panels; - var wrapper = info.wrapper; - var cmWrapper = this.getWrapperElement(); - - if (options.after instanceof Panel && !options.after.cleared) { - wrapper.insertBefore(node, options.before.node.nextSibling); - } else if (options.before instanceof Panel && !options.before.cleared) { - wrapper.insertBefore(node, options.before.node); - } else if (options.replace instanceof Panel && !options.replace.cleared) { - wrapper.insertBefore(node, options.replace.node); - options.replace.clear(); - } else if (options.position == "bottom") { - wrapper.appendChild(node); - } else if (options.position == "before-bottom") { - wrapper.insertBefore(node, cmWrapper.nextSibling); - } else if (options.position == "after-top") { - wrapper.insertBefore(node, cmWrapper); - } else { - wrapper.insertBefore(node, wrapper.firstChild); - } - - var height = (options && options.height) || node.offsetHeight; - this._setSize(null, info.heightLeft -= height); - info.panels++; - return new Panel(this, node, options, height); - }); - - function Panel(cm, node, options, height) { - this.cm = cm; - this.node = node; - this.options = options; - this.height = height; - this.cleared = false; - } - - Panel.prototype.clear = function() { - if (this.cleared) return; - this.cleared = true; - var info = this.cm.state.panels; - this.cm._setSize(null, info.heightLeft += this.height); - info.wrapper.removeChild(this.node); - if (--info.panels == 0) removePanels(this.cm); - }; - - Panel.prototype.changed = function(height) { - var newHeight = height == null ? this.node.offsetHeight : height; - var info = this.cm.state.panels; - this.cm._setSize(null, info.height += (newHeight - this.height)); - this.height = newHeight; - }; - - function initPanels(cm) { - var wrap = cm.getWrapperElement(); - var style = window.getComputedStyle ? window.getComputedStyle(wrap) : wrap.currentStyle; - var height = parseInt(style.height); - var info = cm.state.panels = { - setHeight: wrap.style.height, - heightLeft: height, - panels: 0, - wrapper: document.createElement("div") - }; - wrap.parentNode.insertBefore(info.wrapper, wrap); - var hasFocus = cm.hasFocus(); - info.wrapper.appendChild(wrap); - if (hasFocus) cm.focus(); - - cm._setSize = cm.setSize; - if (height != null) cm.setSize = function(width, newHeight) { - if (newHeight == null) return this._setSize(width, newHeight); - info.setHeight = newHeight; - if (typeof newHeight != "number") { - var px = /^(\d+\.?\d*)px$/.exec(newHeight); - if (px) { - newHeight = Number(px[1]); - } else { - info.wrapper.style.height = newHeight; - newHeight = info.wrapper.offsetHeight; - info.wrapper.style.height = ""; - } - } - cm._setSize(width, info.heightLeft += (newHeight - height)); - height = newHeight; - }; - } - - function removePanels(cm) { - var info = cm.state.panels; - cm.state.panels = null; - - var wrap = cm.getWrapperElement(); - info.wrapper.parentNode.replaceChild(wrap, info.wrapper); - wrap.style.height = info.setHeight; - cm.setSize = cm._setSize; - cm.setSize(); - } -}); |