diff --git a/lib/ace/edit_session.js b/lib/ace/edit_session.js index 44a83ff1..98125892 100644 --- a/lib/ace/edit_session.js +++ b/lib/ace/edit_session.js @@ -439,15 +439,11 @@ var EditSession = function(text, mode) { 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.$useWorker = useWorker; + + this.$stopWorker(); + if (useWorker) + this.$startWorker(); }; this.getUseWorker = function() { @@ -463,14 +459,12 @@ var EditSession = function(text, mode) { this.$mode = null; this.setMode = function(mode) { if (this.$mode === mode) return; + this.$mode = mode; - if (this.$worker) - this.$worker.terminate(); + this.$stopWorker(); - if (this.$useWorker && typeof Worker !== "undefined" && !require.noWorker) - this.$worker = mode.createWorker(this); - else - this.$worker = null; + if (this.$useWorker) + this.$startWorker(); var tokenizer = mode.getTokenizer(); @@ -492,10 +486,30 @@ var EditSession = function(text, mode) { this.bgTokenizer.setDocument(this.getDocument()); this.bgTokenizer.start(0); - this.$mode = mode; this._dispatchEvent("changeMode"); }; + this.$stopWorker = function() { + if (this.$worker) + this.$worker.terminate(); + + this.$worker = null; + }; + + this.$startWorker = function() { + if (typeof Worker !== "undefined" && !require.noWorker) { + try { + this.$worker = this.$mode.createWorker(this); + } catch (e) { + console.log("Could not load worker"); + console.log(e); + this.$worker = null; + } + } + else + this.$worker = null; + }; + this.getMode = function() { return this.$mode; };