summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
-rw-r--r--index.html1
-rw-r--r--js/codemirror/panel.js112
2 files changed, 0 insertions, 113 deletions
diff --git a/index.html b/index.html
index 15885a6..618711e 100644
--- a/index.html
+++ b/index.html
@@ -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();
- }
-});