| /**
 * Storage and control for undo information within a CodeMirror
 * editor. 'Why on earth is such a complicated mess required for
 * that?', I hear you ask. The goal, in implementing this, was to make
 * the complexity of storing and reverting undo information depend
 * only on the size of the edited or restored content, not on the size
 * of the whole document. This makes it necessary to use a kind of
 * 'diff' system, which, when applied to a DOM tree, causes some
 * complexity and hackery.
 *
 * In short, the editor 'touches' BR elements as it parses them, and
 * the History stores these. When nothing is touched in commitDelay
 * milliseconds, the changes are committed: It goes over all touched
 * nodes, throws out the ones that did not change since last commit or
 * are no longer in the document, and assembles the rest into zero or
 * more 'chains' -- arrays of adjacent lines. Links back to these
 * chains are added to the BR nodes, while the chain that previously
 * spanned these nodes is added to the undo history. Undoing a change
 * means taking such a chain off the undo history, restoring its
 * content (text is saved per line) and linking it back into the
 * document.
 */
// A history object needs to know about the DOM container holding the
// document, the maximum amount of undo levels it should store, the
// delay (of no input) after which it commits a set of changes, and,
// unfortunately, the 'parent' window -- a window that is not in
// designMode, and on which setTimeout works in every browser.
function History(container, maxDepth, commitDelay, editor) {
    this.container = container;
    this.maxDepth = maxDepth;
    this.commitDelay = commitDelay;
    this.editor = editor;
    this.parent = editor.parent;
    // This line object represents the initial, empty editor.
    var initial = {text: "", from: null, to: null};
    // As the borders between lines are represented by BR elements, the
    // start of the first line and the end of the last one are
    // represented by null. Since you can not store any properties
    // (links to line objects) in null, these properties are used in
    // those cases.
    this.first = initial;
    this.last = initial;
    // Similarly, a 'historyTouched' property is added to the BR in
    // front of lines that have already been touched, and 'firstTouched'
    // is used for the first line.
    this.firstTouched = false;
    // History is the set of committed changes, touched is the set of
    // nodes touched since the last commit.
    this.history = [];
    this.redoHistory = [];
    this.touched = [];
}
History.prototype = {
    // Schedule a commit (if no other touches come in for commitDelay
    // milliseconds).
    scheduleCommit: function () {
        var self = this;
        this.parent.clearTimeout(this.commitTimeout);
        this.commitTimeout = this.parent.setTimeout(function () {
            self.tryCommit();
        }, this.commitDelay);
    },
    // Mark a node as touched. Null is a valid argument.
    touch: function (node) {
        this.setTouched(node);
        this.scheduleCommit();
    },
    // Undo the last change.
    undo: function () {
        // Make sure pending changes have been committed.
        this.commit();
        if (this.history.length) {
            // Take the top diff from the history, apply it, and store its
            // shadow in the redo history.
            var item = this.history.pop();
            this.redoHistory.push(this.updateTo(item, "applyChain"));
            this.notifyEnvironment();
            return this.chainNode(item);
        }
    },
    // Redo the last undone change.
    redo: function () {
        this.commit();
        if (this.redoHistory.length) {
            // The inverse of undo, basically.
            var item = this.redoHistory.pop();
            this.addUndoLevel(this.updateTo(item, "applyChain"));
            this.notifyEnvironment();
            return this.chainNode(item);
        }
    },
    clear: function () {
        this.history = [];
        this.redoHistory = [];
    },
    // Ask for the size of the un/redo histories.
    historySize: function () {
        return {undo: this.history.length, redo: this.redoHistory.length};
    },
    // Push a changeset into the document.
    push: function (from, to, lines) {
        var chain = [];
        for (var i = 0; i < lines.length; i++) {
            var end = (i == lines.length - 1) ? to : this.container.ownerDocument.createElement("BR");
            chain.push({from: from, to: end, text: cleanText(lines[i])});
            from = end;
        }
        this.pushChains([chain], from == null && to == null);
        this.notifyEnvironment();
    },
    pushChains: function (chains, doNotHighlight) {
        this.commit(doNotHighlight);
        this.addUndoLevel(this.updateTo(chains, "applyChain"));
        this.redoHistory = [];
    },
    // Retrieve a DOM node from a chain (for scrolling to it after undo/redo).
    chainNode: function (chains) {
        for (var i = 0; i < chains.length; i++) {
            var start = chains[i][0], node = start && (start.from || start.to);
            if (node) return node;
        }
    },
    // Clear the undo history, make the current document the start
    // position.
    reset: function () {
        this.history = [];
        this.redoHistory = [];
    },
    textAfter: function (br) {
        return this.after(br).text;
    },
    nodeAfter: function (br) {
        return this.after(br).to;
    },
    nodeBefore: function (br) {
        return this.before(br).from;
    },
    // Commit unless there are pending dirty nodes.
    tryCommit: function () {
        if (!window.History) return; // Stop when frame has been unloaded
        if (this.editor.highlightDirty()) this.commit(true);
        else this.scheduleCommit();
    },
    // Check whether the touched nodes hold any changes, if so, commit
    // them.
    commit: function (doNotHighlight) {
        this.parent.clearTimeout(this.commitTimeout);
        // Make sure there are no pending dirty nodes.
        if (!doNotHighlight) this.editor.highlightDirty(true);
        // Build set of chains.
        var chains = this.touchedChains(), self = this;
        if (chains.length) {
            this.addUndoLevel(this.updateTo(chains, "linkChain"));
            this.redoHistory = [];
            this.notifyEnvironment();
        }
    },
    // [ end of public interface ]
    // Update the document with a given set of chains, return its
    // shadow. updateFunc should be "applyChain" or "linkChain". In the
    // second case, the chains are taken to correspond the the current
    // document, and only the state of the line data is updated. In the
    // first case, the content of the chains is also pushed iinto the
    // document.
    updateTo: function (chains, updateFunc) {
        var shadows = [], dirty = [];
        for (var i = 0; i < chains.length; i++) {
            shadows.push(this.shadowChain(chains[i]));
            dirty.push(this[updateFunc](chains[i]));
        }
        if (updateFunc == "applyChain")
            this.notifyDirty(dirty);
        return shadows;
    },
    // Notify the editor that some nodes have changed.
    notifyDirty: function (nodes) {
        forEach(nodes, method(this.editor, "addDirtyNode"))
        this.editor.scheduleHighlight();
    },
    notifyEnvironment: function () {
        // Used by the line-wrapping line-numbering code.
        if (window.frameElement && window.frameElement.CodeMirror.updateNumbers)
            window.frameElement.CodeMirror.updateNumbers();
        if (this.onChange) this.onChange();
    },
    // Link a chain into the DOM nodes (or the first/last links for null
    // nodes).
    linkChain: function (chain) {
        for (var i = 0; i < chain.length; i++) {
            var line = chain[i];
            if (line.from) line.from.historyAfter = line;
            else this.first = line;
            if (line.to) line.to.historyBefore = line;
            else this.last = line;
        }
    },
    // Get the line object after/before a given node.
    after: function (node) {
        return node ? node.historyAfter : this.first;
    },
    before: function (node) {
        return node ? node.historyBefore : this.last;
    },
    // Mark a node as touched if it has not already been marked.
    setTouched: function (node) {
        if (node) {
            if (!node.historyTouched) {
                this.touched.push(node);
                node.historyTouched = true;
            }
        }
        else {
            this.firstTouched = true;
        }
    },
    // Store a new set of undo info, throw away info if there is more of
    // it than allowed.
    addUndoLevel: function (diffs) {
        this.history.push(diffs);
        if (this.history.length > this.maxDepth)
            this.history.shift();
    },
    // Build chains from a set of touched nodes.
    touchedChains: function () {
        var self = this;
        // The temp system is a crummy hack to speed up determining
        // whether a (currently touched) node has a line object associated
        // with it. nullTemp is used to store the object for the first
        // line, other nodes get it stored in their historyTemp property.
        var nullTemp = null;
        function temp(node) {
            return node ? node.historyTemp : nullTemp;
        }
        function setTemp(node, line) {
            if (node) node.historyTemp = line;
            else nullTemp = line;
        }
        function buildLine(node) {
            var text = [];
            for (var cur = node ? node.nextSibling : self.container.firstChild;
                 cur && !isBR(cur); cur = cur.nextSibling)
                if (cur.currentText) text.push(cur.currentText);
            return {from: node, to: cur, text: cleanText(text.join(""))};
        }
        // Filter out unchanged lines and nodes that are no longer in the
        // document. Build up line objects for remaining nodes.
        var lines = [];
        if (self.firstTouched) self.touched.push(null);
        forEach(self.touched, function (node) {
            if (node && node.parentNode != self.container) return;
            if (node) node.historyTouched = false;
            else self.firstTouched = false;
            var line = buildLine(node), shadow = self.after(node);
            if (!shadow || shadow.text != line.text || shadow.to != line.to) {
                lines.push(line);
                setTemp(node, line);
            }
        });
        // Get the BR element after/before the given node.
        function nextBR(node, dir) {
            var link = dir + "Sibling", search = node[link];
            while (search && !isBR(search))
                search = search[link];
            return search;
        }
        // Assemble line objects into chains by scanning the DOM tree
        // around them.
        var chains = [];
        self.touched = [];
        forEach(lines, function (line) {
            // Note that this makes the loop skip line objects that have
            // been pulled into chains by lines before them.
            if (!temp(line.from)) return;
            var chain = [], curNode = line.from, safe = true;
            // Put any line objects (referred to by temp info) before this
            // one on the front of the array.
            while (true) {
                var curLine = temp(curNode);
                if (!curLine) {
                    if (safe) break;
                    else curLine = buildLine(curNode);
                }
                chain.unshift(curLine);
                setTemp(curNode, null);
                if (!curNode) break;
                safe = self.after(curNode);
                curNode = nextBR(curNode, "previous");
            }
            curNode = line.to;
            safe = self.before(line.from);
            // Add lines after this one at end of array.
            while (true) {
                if (!curNode) break;
                var curLine = temp(curNode);
                if (!curLine) {
                    if (safe) break;
                    else curLine = buildLine(curNode);
                }
                chain.push(curLine);
                setTemp(curNode, null);
                safe = self.before(curNode);
                curNode = nextBR(curNode, "next");
            }
            chains.push(chain);
        });
        return chains;
    },
    // Find the 'shadow' of a given chain by following the links in the
    // DOM nodes at its start and end.
    shadowChain: function (chain) {
        var shadows = [], next = this.after(chain[0].from), end = chain[chain.length - 1].to;
        while (true) {
            shadows.push(next);
            var nextNode = next.to;
            if (!nextNode || nextNode == end)
                break;
            else
                next = nextNode.historyAfter || this.before(end);
            // (The this.before(end) is a hack -- FF sometimes removes
            // properties from BR nodes, in which case the best we can hope
            // for is to not break.)
        }
        return shadows;
    },
    // Update the DOM tree to contain the lines specified in a given
    // chain, link this chain into the DOM nodes.
    applyChain: function (chain) {
        // Some attempt is made to prevent the cursor from jumping
        // randomly when an undo or redo happens. It still behaves a bit
        // strange sometimes.
        var cursor = select.cursorPos(this.container, false), self = this;
        // Remove all nodes in the DOM tree between from and to (null for
        // start/end of container).
        function removeRange(from, to) {
            var pos = from ? from.nextSibling : self.container.firstChild;
            while (pos != to) {
                var temp = pos.nextSibling;
                removeElement(pos);
                pos = temp;
            }
        }
        var start = chain[0].from, end = chain[chain.length - 1].to;
        // Clear the space where this change has to be made.
        removeRange(start, end);
        // Insert the content specified by the chain into the DOM tree.
        for (var i = 0; i < chain.length; i++) {
            var line = chain[i];
            // The start and end of the space are already correct, but BR
            // tags inside it have to be put back.
            if (i > 0)
                self.container.insertBefore(line.from, end);
            // Add the text.
            var node = makePartSpan(fixSpaces(line.text), this.container.ownerDocument);
            self.container.insertBefore(node, end);
            // See if the cursor was on this line. Put it back, adjusting
            // for changed line length, if it was.
            if (cursor && cursor.node == line.from) {
                var cursordiff = 0;
                var prev = this.after(line.from);
                if (prev && i == chain.length - 1) {
                    // Only adjust if the cursor is after the unchanged part of
                    // the line.
                    for (var match = 0; match < cursor.offset &&
                    line.text.charAt(match) == prev.text.charAt(match); match++);
                    if (cursor.offset > match)
                        cursordiff = line.text.length - prev.text.length;
                }
                select.setCursorPos(this.container, {node: line.from, offset: Math.max(0, cursor.offset + cursordiff)});
            }
            // Cursor was in removed line, this is last new line.
            else if (cursor && (i == chain.length - 1) && cursor.node && cursor.node.parentNode != this.container) {
                select.setCursorPos(this.container, {node: line.from, offset: line.text.length});
            }
        }
        // Anchor the chain in the DOM tree.
        this.linkChain(chain);
        return start;
    }
};
 |