From c233b266a20832fc7727ee572e22053239a93dee Mon Sep 17 00:00:00 2001
From: Emilio Jesus Gallego Arias <e+git@x80.org>
Date: Fri, 5 Apr 2024 18:59:19 +0200
Subject: [PATCH] [vscode] Add simple commands to move backwards / forward in a
 proof.

We add two new VSCode commands to allow to move one sentence backwards
/ forward, this is particularly useful when combined with lazy
checking mode

The code is very hacky, and fully client-side, improvements and
further ideas most welcome!

Fixes #263, fixes #580.

I'd propose Meta-n and Meta-P as default keybindings, what do you
folks think?
---
 CHANGES.md                |  3 +++
 editor/code/package.json  |  8 +++++++
 editor/code/src/client.ts |  5 ++++-
 editor/code/src/edit.ts   | 45 +++++++++++++++++++++++++++++++++++++++
 4 files changed, 60 insertions(+), 1 deletion(-)
 create mode 100644 editor/code/src/edit.ts

diff --git a/CHANGES.md b/CHANGES.md
index 17488aa7a..c42406bc3 100644
--- a/CHANGES.md
+++ b/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
 -----------------------------
diff --git a/editor/code/package.json b/editor/code/package.json
index 8c0488465..659f7cf18 100644
--- a/editor/code/package.json
+++ b/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": [
diff --git a/editor/code/src/client.ts b/editor/code/src/client.ts
index 83306de55..2efaf6001 100644
--- a/editor/code/src/client.ts
+++ b/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();
diff --git a/editor/code/src/edit.ts b/editor/code/src/edit.ts
new file mode 100644
index 000000000..e01c64a2a
--- /dev/null
+++ b/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);
+  }
+}