add option to turn off workers

This commit is contained in:
Fabian Jakobs 2011-02-21 10:10:57 +01:00
commit 527fcff5f5

View file

@ -344,6 +344,24 @@ var EditSession = function(text, mode) {
return this.doc.getNewLineMode();
};
this.$useWorker = true;
this.setUseWorker = function(useWorker) {
if (this.$useWorker == useWorker)
return;
if (useWorker && !this.$worker && window.Worker)
this.$worker = mode.createWorker(this);
if (!useWorker && this.$worker) {
this.$worker.terminate();
this.$worker = null;
}
};
this.getUseWorker = function() {
return this.$useWorker;
};
this.$mode = null;
this.setMode = function(mode) {
if (this.$mode === mode) return;
@ -351,7 +369,7 @@ var EditSession = function(text, mode) {
if (this.$worker)
this.$worker.terminate();
if (window.Worker && !require.noWorker)
if (this.$useWorker && window.Worker && !require.noWorker)
this.$worker = mode.createWorker(this);
else
this.$worker = null;