From 9c060bc5b599692d3026fd69641ecbaae5b475c2 2014-12-07 21:10:15
From: Min RK <benjaminrk@gmail.com>
Date: 2014-12-07 21:10:15
Subject: [PATCH] setting an option to null sets the default in CodeMirror

matching the unset behavior in config

---

diff --git a/IPython/html/static/edit/js/editor.js b/IPython/html/static/edit/js/editor.js
index 6895254..4a0a453 100644
--- a/IPython/html/static/edit/js/editor.js
+++ b/IPython/html/static/edit/js/editor.js
@@ -116,8 +116,11 @@ function($,
             if (!options.hasOwnProperty(opt)) {
                 continue;
             }
-            console.log(opt, options[opt]);
-            this.codemirror.setOption(opt, options[opt]);
+            var value = options[opt];
+            if (value === null) {
+                value = CodeMirror.defaults[opt];
+            }
+            this.codemirror.setOption(opt, value);
         }
     };