Merge pull request #718 from ejgallego/next_back_keybindings

[code] Add keybindings for sentenceNext / sentencePrevious

CHANGES.md

@@ -75,6 +75,9 @@
  - new VSCode commands to allow to move one sentence backwards /
    forward, this is particularly useful when combined with lazy
    checking mode (@ejgallego, #671, fixes #263, fixes #580)
+ - VSCode commands `coq-lsp.sentenceNext` / `coq-lsp.sentencePrevious`
+   are now bound by default to `Alt + N` / `Alt + P` keybindings
+   (@ejgallego, #718)
  - change diagnostic `extra` field to `data`, so we now conform to the
    LSP spec, include the data only when the `send_diags_extra_data`
    server-side option is enabled (@ejgallego, #670)
@@ -135,8 +138,11 @@
    the scheduler for the visible area of the document; combined with
    the new lazy checking mode, this provides checking on scroll, a
    feature inspired from Isabelle IDE (@ejgallego, #717)
- - Have VSCode wait for full LSP client shutdown on server restart
+ - Have VSCode wait for full LSP client shutdown on server
+   restart. This fixes some bugs on extension restart (finally!)
    (@ejgallgo, #719)
+ - Center the view if cursor goes out of scope in
+   `sentenceNext/sentencePrevious` (@ejgallego, #718)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

editor/code/package.json

@@ -111,7 +111,7 @@
         "title": "Coq LSP: try to jump to next Coq sentence"
       },
       {
-        "command": "coq-lsp.sentenceBack",
+        "command": "coq-lsp.sentencePrevious",
         "title": "Coq LSP: try to jump to previous Coq sentence"
       },
       {
@@ -125,6 +125,18 @@
         "key": "alt+enter",
         "mac": "meta+enter",
         "when": "editorTextFocus && (editorLangId == coq || editorTextFocus && editorLangId == markdown)"
+      },
+      {
+        "command": "coq-lsp.sentenceNext",
+        "key": "Alt+N",
+        "mac": "cmd+N",
+        "when": "editorTextFocus && (editorLangId == coq || editorTextFocus && editorLangId == markdown)"
+      },
+      {
+        "command": "coq-lsp.sentencePrevious",
+        "key": "Alt+P",
+        "mac": "cmd+P",
+        "when": "editorTextFocus && (editorLangId == coq || editorTextFocus && editorLangId == markdown)"
       }
     ],
     "viewsContainers": {

editor/code/src/client.ts

@@ -45,7 +45,7 @@ import { CoqLspClientConfig, CoqLspServerConfig, CoqSelector } from "./config";
 import { InfoPanel, goalReq } from "./goals";
 import { FileProgressManager } from "./progress";
 import { coqPerfData, PerfDataView } from "./perf";
-import { sentenceNext, sentenceBack } from "./edit";
+import { sentenceNext, sentencePrevious } from "./edit";
 import { HeatMap, HeatMapConfig } from "./heatmap";
 import { debounce, throttle } from "throttle-debounce";
 
@@ -461,7 +461,7 @@ export function activateCoqLSP(
   coqEditorCommand("save", saveDocument);
 
   coqEditorCommand("sentenceNext", sentenceNext);
-  coqEditorCommand("sentenceBack", sentenceBack);
+  coqEditorCommand("sentencePrevious", sentencePrevious);
 
   coqEditorCommand("heatmap.toggle", heatMapToggle);
 

editor/code/src/edit.ts

@@ -1,7 +1,23 @@
 // Edition facilities for Coq files
-import { TextEditor, Position, Range, Selection } from "vscode";
+import {
+  TextEditor,
+  Position,
+  Range,
+  Selection,
+  TextEditorRevealType,
+} from "vscode";
 
-export function sentenceBack(editor: TextEditor) {
+function setSelection(editor: TextEditor, newCursor: Position) {
+  editor.selection = new Selection(newCursor, newCursor);
+
+  // Is there not a better way?
+  editor.revealRange(
+    new Range(newCursor, newCursor),
+    TextEditorRevealType.InCenterIfOutsideViewport
+  );
+}
+
+export function sentencePrevious(editor: TextEditor) {
   // Slice from the beginning of the document
   let cursor = editor.selection.active;
   let range = new Range(editor.document.positionAt(0), cursor);
@@ -19,7 +35,7 @@ export function sentenceBack(editor: TextEditor) {
       index = text.lastIndexOf(match) + match.length;
     }
     let newCursor = editor.document.positionAt(index);
-    editor.selection = new Selection(newCursor, newCursor);
+    setSelection(editor, newCursor);
   }
 }
 
@@ -40,6 +56,6 @@ export function sentenceNext(editor: TextEditor) {
     let newCursor = editor.document.positionAt(
       editor.document.offsetAt(cursor) + index
     );
-    editor.selection = new Selection(newCursor, newCursor);
+    setSelection(editor, newCursor);
   }
 }

etc/doc/USER_MANUAL.md

@@ -46,8 +46,12 @@ facilities. In VSCode, these settings can be usually displayed in the
 ### Goal display
 
 By default, `coq-lsp` will follow cursor and show goals at cursor
-position. This can be tweaked in options. There are commands to move
-one Coq sentence forward / backwards.
+position. This can be tweaked in options.
+
+The `coq-lsp.sentenceNext` and `coq-lsp.sentencePrevious` commands will
+try to move the cursor one Coq sentence forward / backwards. These
+commands are bound by default to `Alt + N` / `Alt + P` (`Cmd` on
+MacOS).
 
 ### Incremental proof edition