
Previously, we were at an ACE editor published between 1.1.8 and 1.1.9. This caused multiple issues and was especially a problem for the upcoming pair programming feature. Further, updating ace is a long-time priority, see https://github.com/openHPI/codeocean/issues/250. Now, we are not yet updating to the latest version, but rather to the next minor version. This already contains breaking changes, and we are currently interested to keep the number of changes as low as possible. Further updating ACE might be still a future task. The new ACE version 1.2.0 is taken from this tag: https://github.com/ajaxorg/ace-builds/releases/tag/v1.2.0. We are using the src build (not minified, not in the noconflict version), since the same was used before as well. Further, we need to change our migration for storing editor events. Since the table is not yet used (in production), we also update the enum.
246 lines
7.2 KiB
JavaScript
246 lines
7.2 KiB
JavaScript
define("ace/split",["require","exports","module","ace/lib/oop","ace/lib/lang","ace/lib/event_emitter","ace/editor","ace/virtual_renderer","ace/edit_session"], function(require, exports, module) {
|
|
"use strict";
|
|
|
|
var oop = require("./lib/oop");
|
|
var lang = require("./lib/lang");
|
|
var EventEmitter = require("./lib/event_emitter").EventEmitter;
|
|
|
|
var Editor = require("./editor").Editor;
|
|
var Renderer = require("./virtual_renderer").VirtualRenderer;
|
|
var EditSession = require("./edit_session").EditSession;
|
|
|
|
|
|
var Split = function(container, theme, splits) {
|
|
this.BELOW = 1;
|
|
this.BESIDE = 0;
|
|
|
|
this.$container = container;
|
|
this.$theme = theme;
|
|
this.$splits = 0;
|
|
this.$editorCSS = "";
|
|
this.$editors = [];
|
|
this.$orientation = this.BESIDE;
|
|
|
|
this.setSplits(splits || 1);
|
|
this.$cEditor = this.$editors[0];
|
|
|
|
|
|
this.on("focus", function(editor) {
|
|
this.$cEditor = editor;
|
|
}.bind(this));
|
|
};
|
|
|
|
(function(){
|
|
|
|
oop.implement(this, EventEmitter);
|
|
|
|
this.$createEditor = function() {
|
|
var el = document.createElement("div");
|
|
el.className = this.$editorCSS;
|
|
el.style.cssText = "position: absolute; top:0px; bottom:0px";
|
|
this.$container.appendChild(el);
|
|
var editor = new Editor(new Renderer(el, this.$theme));
|
|
|
|
editor.on("focus", function() {
|
|
this._emit("focus", editor);
|
|
}.bind(this));
|
|
|
|
this.$editors.push(editor);
|
|
editor.setFontSize(this.$fontSize);
|
|
return editor;
|
|
};
|
|
|
|
this.setSplits = function(splits) {
|
|
var editor;
|
|
if (splits < 1) {
|
|
throw "The number of splits have to be > 0!";
|
|
}
|
|
|
|
if (splits == this.$splits) {
|
|
return;
|
|
} else if (splits > this.$splits) {
|
|
while (this.$splits < this.$editors.length && this.$splits < splits) {
|
|
editor = this.$editors[this.$splits];
|
|
this.$container.appendChild(editor.container);
|
|
editor.setFontSize(this.$fontSize);
|
|
this.$splits ++;
|
|
}
|
|
while (this.$splits < splits) {
|
|
this.$createEditor();
|
|
this.$splits ++;
|
|
}
|
|
} else {
|
|
while (this.$splits > splits) {
|
|
editor = this.$editors[this.$splits - 1];
|
|
this.$container.removeChild(editor.container);
|
|
this.$splits --;
|
|
}
|
|
}
|
|
this.resize();
|
|
};
|
|
this.getSplits = function() {
|
|
return this.$splits;
|
|
};
|
|
this.getEditor = function(idx) {
|
|
return this.$editors[idx];
|
|
};
|
|
this.getCurrentEditor = function() {
|
|
return this.$cEditor;
|
|
};
|
|
this.focus = function() {
|
|
this.$cEditor.focus();
|
|
};
|
|
this.blur = function() {
|
|
this.$cEditor.blur();
|
|
};
|
|
this.setTheme = function(theme) {
|
|
this.$editors.forEach(function(editor) {
|
|
editor.setTheme(theme);
|
|
});
|
|
};
|
|
this.setKeyboardHandler = function(keybinding) {
|
|
this.$editors.forEach(function(editor) {
|
|
editor.setKeyboardHandler(keybinding);
|
|
});
|
|
};
|
|
this.forEach = function(callback, scope) {
|
|
this.$editors.forEach(callback, scope);
|
|
};
|
|
|
|
|
|
this.$fontSize = "";
|
|
this.setFontSize = function(size) {
|
|
this.$fontSize = size;
|
|
this.forEach(function(editor) {
|
|
editor.setFontSize(size);
|
|
});
|
|
};
|
|
|
|
this.$cloneSession = function(session) {
|
|
var s = new EditSession(session.getDocument(), session.getMode());
|
|
|
|
var undoManager = session.getUndoManager();
|
|
if (undoManager) {
|
|
var undoManagerProxy = new UndoManagerProxy(undoManager, s);
|
|
s.setUndoManager(undoManagerProxy);
|
|
}
|
|
s.$informUndoManager = lang.delayedCall(function() { s.$deltas = []; });
|
|
s.setTabSize(session.getTabSize());
|
|
s.setUseSoftTabs(session.getUseSoftTabs());
|
|
s.setOverwrite(session.getOverwrite());
|
|
s.setBreakpoints(session.getBreakpoints());
|
|
s.setUseWrapMode(session.getUseWrapMode());
|
|
s.setUseWorker(session.getUseWorker());
|
|
s.setWrapLimitRange(session.$wrapLimitRange.min,
|
|
session.$wrapLimitRange.max);
|
|
s.$foldData = session.$cloneFoldData();
|
|
|
|
return s;
|
|
};
|
|
this.setSession = function(session, idx) {
|
|
var editor;
|
|
if (idx == null) {
|
|
editor = this.$cEditor;
|
|
} else {
|
|
editor = this.$editors[idx];
|
|
}
|
|
var isUsed = this.$editors.some(function(editor) {
|
|
return editor.session === session;
|
|
});
|
|
|
|
if (isUsed) {
|
|
session = this.$cloneSession(session);
|
|
}
|
|
editor.setSession(session);
|
|
return session;
|
|
};
|
|
this.getOrientation = function() {
|
|
return this.$orientation;
|
|
};
|
|
this.setOrientation = function(orientation) {
|
|
if (this.$orientation == orientation) {
|
|
return;
|
|
}
|
|
this.$orientation = orientation;
|
|
this.resize();
|
|
};
|
|
this.resize = function() {
|
|
var width = this.$container.clientWidth;
|
|
var height = this.$container.clientHeight;
|
|
var editor;
|
|
|
|
if (this.$orientation == this.BESIDE) {
|
|
var editorWidth = width / this.$splits;
|
|
for (var i = 0; i < this.$splits; i++) {
|
|
editor = this.$editors[i];
|
|
editor.container.style.width = editorWidth + "px";
|
|
editor.container.style.top = "0px";
|
|
editor.container.style.left = i * editorWidth + "px";
|
|
editor.container.style.height = height + "px";
|
|
editor.resize();
|
|
}
|
|
} else {
|
|
var editorHeight = height / this.$splits;
|
|
for (var i = 0; i < this.$splits; i++) {
|
|
editor = this.$editors[i];
|
|
editor.container.style.width = width + "px";
|
|
editor.container.style.top = i * editorHeight + "px";
|
|
editor.container.style.left = "0px";
|
|
editor.container.style.height = editorHeight + "px";
|
|
editor.resize();
|
|
}
|
|
}
|
|
};
|
|
|
|
}).call(Split.prototype);
|
|
|
|
|
|
function UndoManagerProxy(undoManager, session) {
|
|
this.$u = undoManager;
|
|
this.$doc = session;
|
|
}
|
|
|
|
(function() {
|
|
this.execute = function(options) {
|
|
this.$u.execute(options);
|
|
};
|
|
|
|
this.undo = function() {
|
|
var selectionRange = this.$u.undo(true);
|
|
if (selectionRange) {
|
|
this.$doc.selection.setSelectionRange(selectionRange);
|
|
}
|
|
};
|
|
|
|
this.redo = function() {
|
|
var selectionRange = this.$u.redo(true);
|
|
if (selectionRange) {
|
|
this.$doc.selection.setSelectionRange(selectionRange);
|
|
}
|
|
};
|
|
|
|
this.reset = function() {
|
|
this.$u.reset();
|
|
};
|
|
|
|
this.hasUndo = function() {
|
|
return this.$u.hasUndo();
|
|
};
|
|
|
|
this.hasRedo = function() {
|
|
return this.$u.hasRedo();
|
|
};
|
|
}).call(UndoManagerProxy.prototype);
|
|
|
|
exports.Split = Split;
|
|
});
|
|
|
|
define("ace/ext/split",["require","exports","module","ace/split"], function(require, exports, module) {
|
|
"use strict";
|
|
module.exports = require("../split");
|
|
|
|
});
|
|
(function() {
|
|
window.require(["ace/ext/split"], function() {});
|
|
})();
|
|
|