next up previous contents index
Next: Copying Text Up: The Text Editor Previous: The Text Editor

Entering Text

  The text  editor is the basic tool which one uses to express anything in the Nuprl system. Even when using the proof editor to construct tree--structured proofs the text editor is constantly needed to communicate with the system; for instance, one uses it to tell Nuprl which proof rule to use. Entry of text in this editor is modeless; one types characters and deletes them as if using an ordinary keyboard. There are no special commands to ``save'' text or to ``write'' text. Text that exists in a window will be read and put in the library automatically when the window is closed.

Within the text editor one moves the cursor by using the mouse or the arrow keys on the keypad. Long moves of the cursor  can be made by striking LONG once or twice before the arrow keys. One LONG LONG } preceding a vertical arrow key moves the cursor up or down four lines; if used before a horizontal arrow key LONG moves the cursor left or right four positions. Two LONG 's move the cursor to the end of the line if they precede a horizontal arrow key; if they precede a vertical arrow key they move the cursor up or down by a screenful. To move the cursor from one edit window to another the JUMP JUMP } key is used.

Text is deleted using the delete key on the terminal or the kill key, KILL . The delete key removes the character to the left of the cursor, while the kill key removes the character at which the cursor is positioned. An entire region of text can be erased using the KILL key on a selected region. To select a region, the cursor is positioned at the beginning of the region and the SEL key is pressed or L is clicked. The cursor is then positioned at the end of the region and SEL is pressed again or L is clicked.gif If the KILL key is used now the entire region is deleted and stored in a special buffer called the kill  buffer. At most one region can be selected at a time; if three endpoints are selected only the last two are remembered. A kill operation causes the system to ``forget'' both the endpoints.



next up previous contents index
Next: Copying Text Up: The Text Editor Previous: The Text Editor



Richard Eaton
Thu Sep 14 08:45:18 EDT 1995