diff --git a/client/src/extension.ts b/client/src/extension.ts index 9e534e18f..138ba9a7c 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 efd0dda1b..be5d41914 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 840313f28..248ef9713 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 b31f4e1f5..d04b89ad3 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 } ->