From 3e3eebaac94efd6f322e29766a3aeef07249693b Mon Sep 17 00:00:00 2001
From: Marijn Haverbeke <marijnh@gmail.com>
Date: Tue, 18 Dec 2012 08:59:30 +0100
Subject: [PATCH] Re-focus old activeElement after patchDisplay

It may have been a widget that was removed and put back again, thus
losing focus.

Issue #1094
---
 lib/codemirror.js | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/lib/codemirror.js b/lib/codemirror.js
index 08b4b8b614..6185179d34 100644
--- a/lib/codemirror.js
+++ b/lib/codemirror.js
@@ -531,7 +531,7 @@ window.CodeMirror = (function() {
   }
 
   function patchDisplay(cm, from, to, intact, updateNumbersFrom) {
-    var dims = getDimensions(cm);
+    var dims = getDimensions(cm), focused = document.activeElement;
     var display = cm.display, lineNumbers = cm.options.lineNumbers;
     // IE does bad things to nodes when .innerHTML = "" is used on a parent
     // we still need widgets and markers intact to add back to the new content later
@@ -571,6 +571,8 @@ window.CodeMirror = (function() {
       ++lineNo;
     });
     while (cur) cur = rm(cur);
+
+    if (document.activeElement != focused && focused.offsetHeight) focused.focus();
   }
 
   function buildLineElement(cm, line, lineNo, dims) {