Give example of the extraKeys option.

Issues codemirror#988, codemirror#742, codemirror#612, etc. show that CodeMirror users tend to:

1. Not find how to make the Tab key insert spaces instead of a tab,
2. Miss how to use extraKeys to easily solve the issue.

Adding an example helps them find a solution immediately.

doc/manual.html

@@ -523,6 +523,17 @@ <h2 id="keymaps">Keymaps</h2>
     for example, <code>Shift-Ctrl-Space</code> would be a valid key
     identifier.</p>
 
+    <p>Common example: map the Tab key to insert spaces instead of a tab
+    character.</p>
+
+    <pre data-lang="javascript">
+{
+  Tab: function(cm) {
+    var spaces = Array(cm.getOption("indentUnit") + 1).join(" ");
+    cm.replaceSelection(spaces, "end", "+input");
+  }
+}</pre>
+
     <p>Alternatively, a character can be specified directly by
     surrounding it in single quotes, for example <code>'$'</code>
     or <code>'q'</code>. Due to limitations in the way browsers fire