[vscode] Add simple commands to move backwards / forward in a proof.

CHANGES.md

@@ -67,6 +67,9 @@
    #513)
  - allow more than one input position in `selectionRange` LSP call
    (@ejgallego, #667, fixes #663)
+ - 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)
 
 # coq-lsp 0.1.8.1: Spring fix
 -----------------------------

editor/code/package.json

@@ -105,6 +105,14 @@
       {
         "command": "coq-lsp.trim",
         "title": "Coq LSP: Request the server to trim caches and compact memory (useful to try reduce memory comsumption)"
+      },
+      {
+        "command": "coq-lsp.sentenceNext",
+        "title": "Coq LSP: try to jump to next Coq sentence"
+      },
+      {
+        "command": "coq-lsp.sentenceBack",
+        "title": "Coq LSP: try to jump to previous Coq sentence"
       }
     ],
     "keybindings": [

editor/code/src/client.ts

@@ -12,7 +12,6 @@ import {
   ThemeColor,
   WorkspaceConfiguration,
   Disposable,
-  DocumentSelector,
   languages,
 } from "vscode";
 
@@ -40,6 +39,7 @@ import {
 import { InfoPanel, goalReq } from "./goals";
 import { FileProgressManager } from "./progress";
 import { coqPerfData, PerfDataView } from "./perf";
+import { sentenceNext, sentenceBack } from "./edit";
 
 let config: CoqLspClientConfig;
 let client: BaseLanguageClient;
@@ -338,6 +338,9 @@ export function activateCoqLSP(
   coqEditorCommand("document", getDocument);
   coqEditorCommand("save", saveDocument);
 
+  coqEditorCommand("sentenceNext", sentenceNext);
+  coqEditorCommand("sentenceBack", sentenceBack);
+
   createEnableButton();
 
   start();

editor/code/src/edit.ts

@@ -0,0 +1,45 @@
+// Edition facilities for Coq files
+import { TextEditor, Position, Range, Selection } from "vscode";
+
+export function sentenceBack(editor: TextEditor) {
+  // Slice from the beginning of the document
+  let cursor = editor.selection.active;
+  let range = new Range(editor.document.positionAt(0), cursor);
+  let text = editor.document.getText(range);
+
+  // what a hack
+  let regres = text.match(/\.\s+/g);
+  if (regres) {
+    let match = regres.at(-2) || "";
+    var index = 0;
+    if (match == regres.at(-1) || "") {
+      let idx = text.lastIndexOf(match);
+      index = text.lastIndexOf(match, idx - 1) + match.length;
+    } else {
+      index = text.lastIndexOf(match) + match.length;
+    }
+    let newCursor = editor.document.positionAt(index);
+    editor.selection = new Selection(newCursor, newCursor);
+  }
+}
+
+export function sentenceNext(editor: TextEditor) {
+  // Slice to the end of the document
+  let cursor = editor.selection.active;
+  let lastLine = editor.document.lineCount - 1;
+  let lastPos = editor.document.lineAt(lastLine).range.end;
+  let range = new Range(cursor, lastPos);
+  let text = editor.document.getText(range);
+
+  // get the offset of the first match
+  let regres = text.match(/\.\s+/);
+  if (regres) {
+    regres;
+    let match: any = regres[0];
+    let index = regres.index + match.length;
+    let newCursor = editor.document.positionAt(
+      editor.document.offsetAt(cursor) + index
+    );
+    editor.selection = new Selection(newCursor, newCursor);
+  }
+}