diff options
| author | Hugo Herbelin | 2018-11-11 13:21:18 +0100 |
|---|---|---|
| committer | Hugo Herbelin | 2018-11-11 15:44:10 +0100 |
| commit | e17da6fc25eb7af0fbf59dfa6f1e3dd34c18edde (patch) | |
| tree | ffb599aaaf83d845d3f11276d5ba698e3826844a /ide | |
| parent | 186d67228018a84a93de024971356249ddbde668 (diff) | |
CoqIDE: Do not rebind up and down in microPG mode.
First, they already work by default. Second, by rebinding them, they
cannot be used any longer in the completion menu, which is a bit
annoying.
Diffstat (limited to 'ide')
| -rw-r--r-- | ide/nanoPG.ml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/ide/nanoPG.ml b/ide/nanoPG.ml index 002722ace9..f2913b1d1d 100644 --- a/ide/nanoPG.ml +++ b/ide/nanoPG.ml @@ -153,13 +153,13 @@ let emacs = insert emacs "Emacs" [] [ i#forward_sentence_end, { s with move = None })); mkE ~mods:mM _a "a" "Move to beginning of sentence" (Motion(fun s i -> i#backward_sentence_start, { s with move = None })); - mkE _n "n" "Move to next line" ~alias:[[],_Down,"DOWN"] (Motion(fun s i -> + mkE _n "n" "Move to next line" (Motion(fun s i -> let orig_off = Option.default i#line_offset s.move in let i = i#forward_line in let new_off = min (i#chars_in_line - 1) orig_off in (if new_off > 0 then i#set_line_offset new_off else i), { s with move = Some orig_off })); - mkE _p "p" "Move to previous line" ~alias:[[],_Up,"UP"] (Motion(fun s i -> + mkE _p "p" "Move to previous line" (Motion(fun s i -> let orig_off = Option.default i#line_offset s.move in let i = i#backward_line in let new_off = min (i#chars_in_line - 1) orig_off in |