Editor Cursors

One navigates around a term by moving a cursor, sometimes called the point  by analogy with emacs. The cursor can be in one of three modes:

term mode

A term mode  cursor is always positioned at some term node of the term tree. The term node it indicated, by highlighting its notation and the notation for all its subtrees. The highlighting is usually achieved by using reverse video; swapping foreground and background colors. In this document we indicate a highlighted region of a term by drawing an outline around it. For example,

i: . j: .

indicates that a term cursor is at the subterm j = i + 1. Occasionally a term has no width  , and a term cursor on such a term is displayed as a thin vertical line. In this document, we indicate such a cursor by .

text mode

The text cursor  is used for editing text in text slots. The cursor is represented as . It is positioned either between two adjacent characters of a text slot, or before the first character, or after the last. For example, consider a text slot containing the text string abcdef . Valid text cursors for this string include

abcdefabc defabcdef

The text cursor is the insertion point for new characters.

There is a potential ambiguity as to which text slot a text cursor is at: consider two adjacent text slots containing the strings aaa and zzz and the following text cursor:

aaa zzz.

Display forms are designed so this kind of situation should never occur.

The text cursor is significantly thinner than the term cursor on a no-width term, so it should be easy to distinguish the two.

screen mode

Certain cursor  motion commands are designed for moving around a term's display character-by-character in much the same way as with a conventional text editor. When moving with these commands the cursor always occupies a single character position on the screen. If possible, the editor uses a text cursor. Otherwise it uses a screen cursor . A screen cursor on a character is displayed by outlining the character.

For example, if we had the following text cursor in a term:

i: . j: . j = i + 1

then a `move-left-one-character' command would leave a screen cursor (indicated by a box) over the .

i: . j: . j = i + 1

In the rest of this document we'll never have to explicitly represent a screen cursor, so all outlined terms should be interpreted as term cursors.