/* CodeMirror main module
*
* Implements the CodeMirror constructor and prototype, which take care
* of initializing the editor frame, and providing the outside interface.
*/
// The CodeMirrorConfig object is used to specify a default
// configuration. If you specify such an object before loading this
// file, the values you put into it will override the defaults given
// below. You can also assign to it after loading.
var CodeMirrorConfig = window.CodeMirrorConfig || {};
var CodeMirror = (function(){
function setDefaults(object, defaults) {
for (var option in defaults) {
if (!object.hasOwnProperty(option))
object[option] = defaults[option];
}
}
function forEach(array, action) {
for (var i = 0; i < array.length; i++)
action(array[i]);
}
// These default options can be overridden by passing a set of
// options to a specific CodeMirror constructor. See manual.html for
// their meaning.
setDefaults(CodeMirrorConfig, {
stylesheet: "",
path: "",
parserfile: [],
basefiles: ["util.js", "stringstream.js", "select.js", "undo.js", "editor.js", "tokenize.js"],
iframeClass: null,
passDelay: 200,
passTime: 50,
lineNumberDelay: 200,
lineNumberTime: 50,
continuousScanning: false,
saveFunction: null,
onChange: null,
undoDepth: 50,
undoDelay: 800,
disableSpellcheck: true,
textWrapping: true,
readOnly: false,
width: "",
height: "300px",
autoMatchParens: false,
parserConfig: null,
tabMode: "indent", // or "spaces", "default", "shift"
reindentOnLoad: false,
activeTokens: null,
cursorActivity: null,
lineNumbers: false,
indentUnit: 2,
domain: null
});
function addLineNumberDiv(container) {
var nums = document.createElement("DIV"),
scroller = document.createElement("DIV");
nums.style.position = "absolute";
nums.style.height = "100%";
if (nums.style.setExpression) {
try {nums.style.setExpression("height", "this.previousSibling.offsetHeight + 'px'");}
catch(e) {} // Seems to throw 'Not Implemented' on some IE8 versions
}
nums.style.top = "0px";
nums.style.overflow = "hidden";
container.appendChild(nums);
scroller.className = "CodeMirror-line-numbers";
nums.appendChild(scroller);
return nums;
}
function frameHTML(options) {
if (typeof options.parserfile == "string")
options.parserfile = [options.parserfile];
if (typeof options.stylesheet == "string")
options.stylesheet = [options.stylesheet];
var html = [""];
// Hack to work around a bunch of IE8-specific problems.
html.push("");
forEach(options.stylesheet, function(file) {
html.push("");
});
forEach(options.basefiles.concat(options.parserfile), function(file) {
html.push("