Term Editor

 

 

$$\langle \rangle$$ Jump to term at mouse cursor. Switch windows 1. In ML text of Top Loop: Evaluate expression. 2. In ML text elsewhere: Insert newline 3. Otherwise: Jump to empty slot

$$\langle \rangle$$ In ML text of Top Loop: Insert newline

$$\langle \rangle$$ With term cursor: delete (and save) term

$$\langle \rangle$$ With text cursor: delete char to right With text cursor: delete char to left

$$\langle \rangle$$ In ML text: open position for term

$$\langle \rangle$$ Quit. Don't act on, or save any changes

$$\langle \rangle$$ Exit. Save contents if appropriate. If tactic in window, run it

$$\langle \rangle$$ In Top Loop: scroll back in history

$$\langle \rangle$$ In Top Loop: scroll forward in history

Table 1 summarizes commands for term editor windows.