Cutting and Pasting

The cut-and-paste commands work on terms, segments of text slots, and segments of text and term sequences. In this section we refer to these collectively as items . Cut items can be saved on a save stack{Cutting and Pasting!save stack. All items on the save stack are represented as terms, and it is often possible to cut one kind of item and then paste into another kind of context. For example, one can cut a term, and paste into text sequence, or cut a segment of text from a text slot, and paste into a term sequence.

We define the following kinds of commands:

• SAVE : does not remove an item, but does push a copy onto the save stack. Same idea as copy-as-kill  in emacs.

• DELETE: remove an item from a buffer, not saving it anywhere.

• CUT: (= SAVE + DELETE) removes an item from a buffer and pushes it onto the top of the save stack. Same idea as kill in emacs , although Nuprl does not append together items cut immediately one after the other.

• PASTE: inserts the item on top of the stack back into a buffer, removing it from the stack.

• PASTE-COPY: inserts the item on top of the stack back into a buffer, not removing it from the stack. Same idea as yank in emacs .

• PASTE-NEXT: Only used immediately after a PASTE. Removes the item just pasted from the buffer, and then does a PASTE. Same idea as yank-next in emacs .

• Basic
• Region