summaryrefslogtreecommitdiff
path: root/js
diff options
context:
space:
mode:
Diffstat (limited to 'js')
-rw-r--r--js/codemirror/panel.js112
-rw-r--r--js/codeq/editor.js30
-rw-r--r--js/codeq/prolog.js4
-rw-r--r--js/codeq/python.js14
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),
generated by cgit v1.2.1 (git 2.18.0) at 2024-12-26 05:16:46 +0000