An Editor Calculus With Undo/Redo

Structure editors provide many potential usability benefits to an end-user by allowing them to edit the AST representation of a program rather than a textual representation of it. In addition, they all but remove syntax errors by only allowing the constructing of programs that are syntactically valid. However, structure editors only rarely include undo/redo functionality into the editor itself, and to the best of our knowledge, an underlying, formal specification for undo/redo has yet to be developed. This paper continues previous work on an editor calculus; we extend the calculus with undo and redo and present a history-based operational semantics of the extension. The history used an underlying graph-based structure, containing a history of user actions in the particular structure editor. We study the expressive power of the calculus, give a simple proof of its Turing-power and use the expressiveness result to show how our history-based extension with undo and redo can be expressed in the original editor calculus.