From 871b32d0986537b2b4434a2d9a7126c8676ebefc Mon Sep 17 00:00:00 2001
From: danyaPostfactum <danya.postfactum@gmail.com>
Date: Thu, 24 May 2012 16:50:05 +1200
Subject: [PATCH 1/3] Set width: auto for .ace_gutter .ace_layer (for IE)

---
 lib/ace/css/editor.css | 1 +
 1 file changed, 1 insertion(+)

diff --git a/lib/ace/css/editor.css b/lib/ace/css/editor.css
index af1cecf3..b38dc453 100644
--- a/lib/ace/css/editor.css
+++ b/lib/ace/css/editor.css
@@ -128,6 +128,7 @@
 .ace_gutter .ace_layer {
     position: relative;
     min-width: 40px;
+    width: auto;
     text-align: right;
     pointer-events: auto;
 }

From ca5023fb8657dea044add57b3f645cfc8525959f Mon Sep 17 00:00:00 2001
From: danyaPostfactum <danya.postfactum@gmail.com>
Date: Thu, 24 May 2012 16:54:08 +1200
Subject: [PATCH 2/3] Fix "self" reference (for IE)

---
 lib/ace/editor.js | 3 ++-
 1 file changed, 2 insertions(+), 1 deletion(-)

diff --git a/lib/ace/editor.js b/lib/ace/editor.js
index ac7c31ac..834e603a 100644
--- a/lib/ace/editor.js
+++ b/lib/ace/editor.js
@@ -509,8 +509,9 @@ var Editor = function(renderer, session) {
             this.$updateHighlightActiveLine();
         }
 
+        var self = this;
         if (this.$highlightSelectedWord && !this.$wordHighlightTimer)
-            this.$wordHighlightTimer = setTimeout(function(self) {
+            this.$wordHighlightTimer = setTimeout(function() {
                 self.session.$mode.highlightSelection(self);
                 self.$wordHighlightTimer = null;
             }, 30, this);

From 217ed2457b94ba4273a35da6565603ff54521c16 Mon Sep 17 00:00:00 2001
From: danyaPostfactum <danya.postfactum@gmail.com>
Date: Thu, 24 May 2012 16:56:03 +1200
Subject: [PATCH 3/3] Allow gutterLineHighlight in IE

---
 lib/ace/virtual_renderer.js | 4 ----
 1 file changed, 4 deletions(-)

diff --git a/lib/ace/virtual_renderer.js b/lib/ace/virtual_renderer.js
index 996315e8..363f3cd8 100644
--- a/lib/ace/virtual_renderer.js
+++ b/lib/ace/virtual_renderer.js
@@ -451,10 +451,6 @@ var VirtualRenderer = function(container, theme) {
 
     this.$highlightGutterLine = false;
     this.setHighlightGutterLine = function(shouldHighlight) {
-        // adding this element to gutter causes strange behavior on ie
-        if (useragent.isIE)
-            return;
-
         if (this.$highlightGutterLine == shouldHighlight)
             return;
         this.$highlightGutterLine = shouldHighlight;