Add getHistory and setHistory methods

doc/manual.html

@@ -541,6 +541,15 @@ <h2 id="api">Programming API</h2>
       undo and redo operations.</dd>
       <dt id="clearHistory"><code>clearHistory()</code></dt>
       <dd>Clears the editor's undo history.</dd>
+      <dt id="getHistory"><code>getHistory() → object</code></dt>
+      <dd>Get a (JSON-serializeable) representation of the undo history.</dd>
+      <dt id="setHistory"><code>setHistory(object)</code></dt>
+      <dd>Replace the editor's undo history with the one provided,
+      which must be a value as returned
+      by <a href="#getHistory"><code>getHistory</code></a>. Note that
+      this will have entirely undefined results if the editor content
+      isn't also the same as it was when <code>getHistory</code> was
+      called.</dd>
 
       <dt id="indentLine"><code>indentLine(line, dir)</code></dt>
       <dd>Reset the given line's indentation to the indentation

lib/codemirror.js

@@ -199,6 +199,15 @@ var CodeMirror = (function() {
       indentSelection: operation(indentSelected),
       historySize: function() {return {undo: history.done.length, redo: history.undone.length};},
       clearHistory: function() {history = new History();},
+      setHistory: function(histData) {
+        history = new History();
+        history.done = histData.done;
+        history.undone = histData.undone;
+      },
+      getHistory: function() {
+        history.time = 0;
+        return {done: history.done.concat([]), undone: history.undone.concat([])};
+      },
       matchBrackets: operation(function(){matchBrackets(true);}),
       getTokenAt: operation(function(pos) {
         pos = clipPos(pos);