A text sequence is a text string in which zero or more characters are replaced with terms. Text sequence s are primarily used for ML code, for comments, and for the left-hand sides of display forms.
The editor presents a text sequence as a display form with alternating text and term slots. A text sequence normally has no left or right delimiters or element separators, in contrast to term sequences. Text sequence s are however easily identified because they usually occur in well-defined contexts.
An example of a text sequence is the ML expression:
With 'n + 1' (D 0)~
THENW TypeCheck~
This text sequence
consists of 3 term slots filled with the terms
'n + 1'
,
~
, and
~
, and 4 text
slots filled with the text strings
With
,
(D 0)
,
THENW TypeCheck
, and
(the null or empty text
string). The
~
's are new-line terms. Keeping new-line
characters out of text strings simplifies the display formatting
algorithm. Usually we make new-line terms invisible, but here we show
them with a printing character for clarity.
The editor supports special operations on text sequence s. For example, you can cut out sub-sequences delimited by any text cursor positions, and paste in at any text cursor position.