Text drawing: effects and selection

[dhardy]

Currently widgets can draw:

• plain text: simple interface and slightly more complex variant (explicit position and viewport)
• text with effects: low-level interface with effect token list
• text with selection: high-level interface with selection range

The latter is a high-level interface giving the theme control over how to draw selection. Possibly unnecessary since there isn't much the theme might want to affect here besides colours.

Currently there is no good way to draw text with effects and selection. If we wanted a merged function text_with_effects_and_selection then the theme would have to merge new tokens into the effects list.

The current effects interface is quite low-level: an ordered list of tokens. These specify colour (index into a specified palette) and whether to underline and/or strike-through. (Font effects are baked into the TextDisplay object; Effect tokens are intended to allow changing underline and font colour without updating the TextDisplay.)

Perhaps a good solution would be to draw underlines/strikethroughs separately from the text: in this case we could replace text_effects with text_underline(.., range) and text_strikethrough(.., range). Except this doesn't allow for drawing selected text with varying colour information, which is required for syntax-highlighted text.