rename document to session

This commit is contained in:
Fabian Jakobs 2011-01-19 09:10:05 +01:00
commit d436d71c20
11 changed files with 147 additions and 139 deletions

View file

@ -102,7 +102,7 @@ exports.launch = function(env) {
var modeEl = document.getElementById("mode");
function setMode() {
env.editor.getDocument().setMode(modes[modeEl.value] || modes.text);
env.editor.getSession().setMode(modes[modeEl.value] || modes.text);
}
modeEl.onchange = setMode;
setMode();
@ -120,7 +120,7 @@ exports.launch = function(env) {
var docEl = document.getElementById("doc");
function onDocChange() {
var doc = docs[docEl.value];
env.editor.setDocument(doc);
env.editor.setSession(doc);
var mode = doc.getMode();
if (mode instanceof JavaScriptMode) {
@ -240,7 +240,7 @@ exports.launch = function(env) {
env.editor.onTextInput(reader.result);
modeEl.value = mode;
env.editor.getDocument().setMode(modes[mode]);
env.editor.getSession().setMode(modes[mode]);
};
reader.readAsText(file);
}