Module Glt_common.Key
type dir=|LEFT|RIGHT|UP|DOWNtype editor_key=|ARROW of dir|PAGE of dir|CHAR of char|CTRL of char|HOME_KEY|END_KEY|DEL_KEY|BACKSPACE|ENTER
val of_char : char -> editor_key
Glt_common.Keytype dir = | LEFT |
| RIGHT |
| UP |
| DOWN |
type editor_key = | ARROW of dir |
| PAGE of dir |
| CHAR of char |
| CTRL of char |
| HOME_KEY |
| END_KEY |
| DEL_KEY |
| BACKSPACE |
| ENTER |
val of_char : char -> editor_key