next up previous contents index
Next: Term Editor Up: Sequences Previous: Term Sequences

Text Sequences

 

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.



Karla Consroe
Wed Oct 23 13:48:45 EDT 1996