diff options
| author | Hugo Herbelin | 2019-04-27 12:38:05 +0200 |
|---|---|---|
| committer | Hugo Herbelin | 2019-04-30 12:56:13 +0200 |
| commit | bae9b53c58d995a0cce404c279c37206e5418d2f (patch) | |
| tree | 0218021d58b771380614121f4a6816fa271840b8 | |
| parent | d42c059d6c7877948fdae76bf0400d4e3b06b90d (diff) | |
CoqIDE nanoPG: adding keys to go the start/end of file (w/o evaluating).
On MacOS X: Ctrl-Cmd-Left and Ctrl-Cmd-Right
Elsewhere: Meta-Left and Meta-Right
See issue #9899 (moving cursor to beginning and end of file).
| -rw-r--r-- | ide/nanoPG.ml | 7 |
1 files changed, 7 insertions, 0 deletions
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index 435076c332..5e6c0b8462 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -160,6 +160,13 @@ let emacs = insert emacs "Emacs" [] [ mkE _e "e" "Move to end of line" (Motion(fun s i -> (if not i#ends_line then i#forward_to_line_end else i), { s with move = None })); + mkE ~mods:mM _Right "->" "Move to end of buffer" (Motion(fun s i -> + i#forward_to_end, + { s with move = None })); + mkE ~mods:mM _Left "<-" "Move to start of buffer" (Motion(fun s i -> + let buffer = new GText.buffer i#buffer in + buffer#start_iter, + { s with move = None })); mkE _a "a" "Move to beginning of line" (Motion(fun s i -> (i#set_line_offset 0), { s with move = None })); mkE ~mods:mM _e "e" "Move to end of sentence" (Motion(fun s i -> |