Re: undo

[bertot@paprika.inria.fr (Yves Bertot)]

Functions like {tree}:replace, {tree}:adopt, and the like and functions
like {variable}:change, {variable}:insert do not serve the same purpose.

The first batch are abstract tree modification primitives.  They only care
about modifying trees, with trying to maintain the coherence of various
tools that might be looking at these trees at the same moment.

The second batch of functions not only enables to modify trees, but also
enables the system to keep various tools handling these trees in a coherent
state.

A basic example is when you have a tree in a "ctedit" window.  The formatter
in the window maintains its own structures for graphical display.  When
the tree is modified, the formatter must be re-run to update its structures
and the display.  The variable is responsible for making this possible.

With a variable, one can record a set of tools (see functions
{variable}:add-tool, {variable}:del-tool, in section "The Path Manual" of the
documentation).  Each time one calls {variable}:change, {variable}:insert, etc...
the variable stores the modification for each recorded tool.
For a given tool which is already recorded, it is possible to ask whether the
tree has been modified (see function {variable}:get-modif) and to say that
the tool is now in a coherent state with the variable (see function
{variable}:reset-tool).

Some tools may be updated at every modification and some tools may be updated
only once in a while.  For this reason, the variable may have to store
several different modification paths.  In this respect, having a function
({variable}:undo variable) would not make much sense.

To implement a form of undo, you have register a tool on your variable that
will decide of the paths to be undone.

Yves.