From 527fcff5f505d1a75835b12737ee87082b3405f3 Mon Sep 17 00:00:00 2001
From: Fabian Jakobs <fabian.jakobs@web.de>
Date: Mon, 21 Feb 2011 10:10:57 +0100
Subject: [PATCH] add option to turn off workers

---
 lib/ace/edit_session.js | 20 +++++++++++++++++++-
 1 file changed, 19 insertions(+), 1 deletion(-)

diff --git a/lib/ace/edit_session.js b/lib/ace/edit_session.js
index 5f8ebc84..8b187fe5 100644
--- a/lib/ace/edit_session.js
+++ b/lib/ace/edit_session.js
@@ -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;