Skip to content

Instantly share code, notes, and snippets.

Embed
What would you like to do?
/* ------- */
// Clean mess from previous session
Cu.import("resource:///modules/source-editor.jsm");
let nbox = gBrowser.getNotificationBox();
while (nbox.lastChild.id == "foobar-container" ||
nbox.lastChild.id == "foobar-splitter") {
nbox.removeChild(nbox.lastChild);
}
/* ------- */
// Build container
let container = document.createElement("vbox");
container.setAttribute("flex", "1");
container.id = "foobar-container";
container.setAttribute("pack", "start");
container.height = 200;
let splitter = document.createElement("splitter");
splitter.className = "devtools-horizontal-splitter";
splitter.id = "foobar-splitter";
nbox.appendChild(splitter);
nbox.appendChild(container);
/* ------- */
// Editor!!!
let input = new SourceEditor();
input.init(container, {
initialText: "/* input */",
}, autofitEditor);
input.editorElement.flex = 0;
function autofitEditor(e) {
let lineHeight = e._view.getLineHeight();
e.previousLineCount = 1;
setEditorSize(e, lineHeight);
e.addEventListener(SourceEditor.EVENTS.TEXT_CHANGED, function() {
let count = e.getLineCount();
if (count != e.previousLineCount) {
e.previousLineCount = count;
setEditorSize(e, lineHeight * count);
}
});
}
function setEditorSize(e, height) {
e.editorElement.style.minHeight =
e.editorElement.style.maxHeight =
e.editorElement.style.height = (4 + height) + "px"; // 4 being the margin
}
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment