text consists of sequences of characters and definition references (also known as def refs). Since these sequences are stored internally as recursive trees, they are also known as text trees, or T-trees . The text editor, ted, is a structure editor for these trees and works in a way similar to that of the Cornell Program Synthesizer; the cursor on the screen represents a cursor into the text tree being edited, and movements of the tree cursor are mapped into movements of the screen's cursor.
The text editor is used to create and modify DEF, ML and EVAL objects as well as rules and main goals of theorems. Changes to objects are reflected immediately; there is no separate ``save'' or ``unsave'' command.
The text editor is almost completely modeless.
To insert a character, type it;
to insert a def, instantiate it;
to remove a character, delete it or KILL
it;
to move the cursor, use the arrow keys;
to exit the editor, use
.
There is a bracket mode, explained in the next section,
which changes the way def refs are displayed.