type special = [
A selection of extra keys on the keyboard.
Things that terminals say to applications.
`Key (k, mods)is keyboard input.
kis a key, one of:
charin the ASCII range;
uis any other unicode character; or
- a special key.
`Uchartogether represent the textual part of the input. These characters are guaranteed not to be control characters, and are safe to use when constructing images. ASCII is separated from the rest of Unicode for convenient pattern-matching.
modsare the extra modifier keys.
`Mouse (event, (x, y), mods)is mouse input.
eventis the actual mouse event:
buttonpress, release, or motion of the mouse with buttons depressed.
(x, y)are column and row position of the mouse. The origin is
(0,0), the upper-left corner.
`Press (`Left|`Middle|`Right)generates a corresponding
`Release, but there is no portable way to detect which button was released.
`Scroll (`Up|`Down)presses are not followed by releases.
`Paste (`Start|`End)are bracketed paste events, signalling the beginning and end of a sequence of events pasted into the terminal.
Note This mechanism is useful, but not reliable. The pasted text could contain spurious start-of-paste or end-of-paste markers, or they could be entered by hand.
Terminal input protocols are historical cruft, and heavily overload the ASCII range. For instance:
- It is impossible to distinguish lower- and upper-case ASCII characters if Ctrl is pressed;
- several combinations of key-presses are aliased as special keys; and
- in a UTF-8 encoded stream, there is no representation for non-ASCII characters with modifier keys.
This means that many values that inhabit the
event type are impossible, while some reflect multiple different user actions. Limitations include:
`Shiftis reported only with special keys, and not all of them.
`Controlare reported with mouse events, key events with special keys, and key events with values in the ranges
~). If Ctrl is pressed, the higher range is mapped into the lower range.
- Terminals will variously under-report modifier key state.
Perform own experiments before relying on elaborate key combinations.
Simple IO-less terminal input processor. It can be used for building custom terminal input abstractions.
Input decoding filter.
The filter should be fed strings, which it first decodes from UTF-8, and then extracts the input events.
Malformed UTF-8 input bytes and unrecognized escape sequences are silently discarded.
val create : unit -> t
create () is a new, empty filter.
val input : t -> bytes -> int -> int -> unit
input t buffer i len feeds
len bytes of
t, starting from position
len = 0 signals the end of input.
buffer is immediately processed and can be reused after the call returns.
val pending : t -> bool
pending t is
true if a call to
next, without any intervening input, would not return
Warning The parsing interface is subject to change.
decode us are the events encoded by
us are assumed to have been generated in a burst, and the end of the list is taken to mean a pause. Therefore,
decode us1 @ decode us2 <> decode (us1 @ us2) if
us1 ends with a partial escape sequence, including a lone
Unsupported escape sequences are silently discarded.