next up previous contents index
Next: Tree CursorsTree Up: System Description Previous: Other Keys in

The Text Editor

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.

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