From 2d8bffff36955d528c515a269dcef9c49ee318a8 Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Fri, 29 Nov 2024 18:08:05 +0100
Subject: [PATCH] fix: stepForward and stepBackward no longer require a
 position to work in continuous mode

---
 client/src/extension.ts                 | 24 ++----------------------
 client/src/manualChecking.ts            |  4 ++--
 language-server/protocol/extProtocol.ml |  2 --
 language-server/vscoqtop/lspManager.ml  |  4 ++--
 4 files changed, 6 insertions(+), 28 deletions(-)

diff --git a/client/src/extension.ts b/client/src/extension.ts
index 9e534e18..138ba9a7 100644
--- a/client/src/extension.ts
+++ b/client/src/extension.ts
@@ -211,28 +211,8 @@ export function activate(context: ExtensionContext) {
         registerVscoqTextCommand('expandAllQueries', () => searchProvider.expandAll());
         registerVscoqTextCommand('interpretToPoint', (editor) => sendInterpretToPoint(editor, client));
         registerVscoqTextCommand('interpretToEnd', (editor) => sendInterpretToEnd(editor, client));
-        registerVscoqTextCommand('stepForward', (editor) => {
-            
-            if(workspace.getConfiguration('vscoq.proof').mode === 1) {
-                const textDocument = makeVersionedDocumentId(editor);
-                const position = editor.selection.active;
-                client.sendNotification("vscoq/stepForward", {textDocument: textDocument, position: position});
-            }
-            else {
-                sendStepForward(editor, client);
-            }
-                
-        });
-        registerVscoqTextCommand('stepBackward', (editor) => {
-            if(workspace.getConfiguration('vscoq.proof').mode === 1) {
-                const textDocument = makeVersionedDocumentId(editor);
-                const position = editor.selection.active;
-                client.sendNotification("vscoq/stepBackward", {textDocument: textDocument, position: position});
-            }
-            else {
-                sendStepBackward(editor, client);
-            }
-        });
+        registerVscoqTextCommand('stepForward', (editor) => sendStepForward(editor, client));
+        registerVscoqTextCommand('stepBackward', (editor) => sendStepBackward(editor, client));
         registerVscoqTextCommand('documentState', async (editor) => {
                 
             documentStateProvider.setDocumentUri(editor.document.uri);
diff --git a/client/src/manualChecking.ts b/client/src/manualChecking.ts
index efd0dda1..be5d4191 100644
--- a/client/src/manualChecking.ts
+++ b/client/src/manualChecking.ts
@@ -27,11 +27,11 @@ export const sendInterpretToEnd = (editor: TextEditor,  client: Client) => {
 
 export const sendStepForward = (editor: TextEditor,  client: Client) => {
     const textDocument = makeVersionedDocumentId(editor);
-    client.sendNotification("vscoq/stepForward", {textDocument: textDocument, position: null});
+    client.sendNotification("vscoq/stepForward", {textDocument: textDocument});
 };
 
 export const sendStepBackward = (editor: TextEditor,  client: Client) => {
     const textDocument = makeVersionedDocumentId(editor);
-    client.sendNotification("vscoq/stepBackward", {textDocument: textDocument, position: null});
+    client.sendNotification("vscoq/stepBackward", {textDocument: textDocument});
 };
 
diff --git a/language-server/protocol/extProtocol.ml b/language-server/protocol/extProtocol.ml
index 840313f2..248ef971 100644
--- a/language-server/protocol/extProtocol.ml
+++ b/language-server/protocol/extProtocol.ml
@@ -42,7 +42,6 @@ module Notification = struct
 
       type t = {
         textDocument : VersionedTextDocumentIdentifier.t;
-        position: Position.t option;
       } [@@deriving yojson]
 
     end
@@ -51,7 +50,6 @@ module Notification = struct
 
       type t = {
         textDocument : VersionedTextDocumentIdentifier.t;
-        position: Position.t option;
       } [@@deriving yojson]
 
     end
diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
index 0b9c20e4..4b613e4c 100644
--- a/language-server/vscoqtop/lspManager.ml
+++ b/language-server/vscoqtop/lspManager.ml
@@ -401,7 +401,7 @@ let coqtopInterpretToPoint params =
     sel_events
  
 let coqtopStepBackward params =
-  let Notification.Client.StepBackwardParams.{ textDocument = { uri }; position } = params in
+  let Notification.Client.StepBackwardParams.{ textDocument = { uri } } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
   | None -> log "[stepBackward] ignoring event on non existent document"; []
   | Some { st; visible } ->
@@ -410,7 +410,7 @@ let coqtopStepBackward params =
       inject_dm_events (uri,events)
 
 let coqtopStepForward params =
-  let Notification.Client.StepForwardParams.{ textDocument = { uri }; position } = params in
+  let Notification.Client.StepForwardParams.{ textDocument = { uri } } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
   | None -> log "[stepForward] ignoring event on non existent document"; []
   | Some { st; visible } ->