diff options
Diffstat (limited to 'js')
-rw-r--r-- | js/codemirror/panel.js | 112 | ||||
-rw-r--r-- | js/codeq/editor.js | 30 | ||||
-rw-r--r-- | js/codeq/prolog.js | 4 | ||||
-rw-r--r-- | js/codeq/python.js | 14 |
4 files changed, 147 insertions, 13 deletions
diff --git a/js/codemirror/panel.js b/js/codemirror/panel.js new file mode 100644 index 0000000..ba29484 --- /dev/null +++ b/js/codemirror/panel.js @@ -0,0 +1,112 @@ +// 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(); + } +}); diff --git a/js/codeq/editor.js b/js/codeq/editor.js new file mode 100644 index 0000000..e7d15f9 --- /dev/null +++ b/js/codeq/editor.js @@ -0,0 +1,30 @@ +codeq.makeEditor = function (elt, options) { + var statusBar = document.createElement("div"), + updateStatusBar = function (pos) { + statusBar.innerHTML = 'line ' + (pos.line+1) + ', column ' + (pos.ch+1); + }, + editor; + + options.cursorHeight = 0.85; + options.lineNumbers = true; + options.matchBrackets = true; + options.extraKeys = { + // replace tabs with spaces + Tab: function (cm) { + var spaces = Array(cm.getOption("indentUnit") + 1).join(" "); + cm.replaceSelection(spaces); + } + }; + editor = CodeMirror(elt, options), + + statusBar.className = 'editor-statusbar'; + updateStatusBar({line: 0, ch: 0}); + + editor.addPanel(statusBar, {position: 'bottom'}); + editor.on('cursorActivity', function (instance) { + var pos = instance.getDoc().getCursor(); + updateStatusBar(pos); + }); + + return editor; +}; diff --git a/js/codeq/prolog.js b/js/codeq/prolog.js index 640aa99..87ac353 100644 --- a/js/codeq/prolog.js +++ b/js/codeq/prolog.js @@ -259,7 +259,9 @@ jqEditor = jqCode.find('.code_editor'), jqTerminal = jqConsole.find('.console'), jqHints = jqInfo.find('.hints'), - editor = CodeMirror(jqEditor[0], { cursorHeight: 0.85, lineNumbers: true, matchBrackets: true }), + editor = codeq.makeEditor(jqEditor[0], { + mode: 'prolog' + }), activityHandler = makeActivityHandler(editor, problemDef.id), terminal = makePrologTerminalHandler(jqTerminal, editor, problemDef.id, activityHandler), hinter = codeq.makeHinter(jqHints, jqEditor, editor, 'prolog_hints', problemDef.hint, commonHints, problemDef.plan), diff --git a/js/codeq/python.js b/js/codeq/python.js index 4724982..e20fe06 100644 --- a/js/codeq/python.js +++ b/js/codeq/python.js @@ -217,19 +217,9 @@ jqEditor = jqCode.find('.code_editor'), jqTerminal = jqConsole.find('.console'), jqHints = jqInfo.find('.hints'), - editor = CodeMirror(jqEditor[0], { - cursorHeight: 0.85, - lineNumbers: true, - matchBrackets: true, + editor = codeq.makeEditor(jqEditor[0], { mode: 'python', - indentUnit: 4, - extraKeys: { - // replace tabs with spaces - Tab: function (cm) { - var spaces = Array(cm.getOption("indentUnit") + 1).join(" "); - cm.replaceSelection(spaces); - } - } + indentUnit: 4 }), activityHandler = makeActivityHandler(editor, problemDef.id), terminal = makePythonTerminalHandler(jqTerminal, editor, problemDef.id, activityHandler), |