fix: stepForward and stepBackward no longer require a position to wor…

…k in continuous mode
coq · Dec 3, 2024 · 2d8bfff · 2d8bfff
1 parent a881fb1
commit 2d8bfff
Show file tree

Hide file tree

Showing 4 changed files with 6 additions and 28 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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 } ->