From 74b3764db29c0cb52219e9baef30ec2f6f05b415 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Thu, 15 Feb 2024 13:47:17 +0100 Subject: [PATCH] Add api for step navigation in continuous mode. Enabled the commands in the client and added the API to handle them in the language server. --- client/package.json | 6 +-- client/src/extension.ts | 28 ++++++++++-- language-server/dm/documentManager.ml | 22 +++++++++ language-server/dm/documentManager.mli | 6 +++ language-server/protocol/extProtocol.ml | 2 + language-server/vscoqtop/lspManager.ml | 60 ++++++++++++++++--------- 6 files changed, 94 insertions(+), 30 deletions(-) diff --git a/client/package.json b/client/package.json index 77c8dfab9..39a44a0fa 100644 --- a/client/package.json +++ b/client/package.json @@ -289,14 +289,12 @@ { "command": "extension.coq.stepForward", "title": "Step Forward", - "category": "Coq", - "enablement": "config.vscoq.proof.mode == 0" + "category": "Coq" }, { "command": "extension.coq.stepBackward", "title": "Step Backward", - "category": "Coq", - "enablement": "config.vscoq.proof.mode == 0" + "category": "Coq" }, { "command": "extension.coq.documentState", diff --git a/client/src/extension.ts b/client/src/extension.ts index c47f5ce50..d9e806f58 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -175,8 +175,28 @@ export function activate(context: ExtensionContext) { registerVscoqTextCommand('expandAllQueries', () => searchProvider.expandAll()); registerVscoqTextCommand('interpretToPoint', (editor) => sendInterpretToPoint(editor, client)); registerVscoqTextCommand('interpretToEnd', (editor) => sendInterpretToEnd(editor, client)); - registerVscoqTextCommand('stepForward', (editor) => sendStepForward(editor, client)); - registerVscoqTextCommand('stepBackward', (editor) => sendStepBackward(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('documentState', async (editor) => { documentStateProvider.setDocumentUri(editor.document.uri); @@ -208,8 +228,8 @@ export function activate(context: ExtensionContext) { const editors = window.visibleTextEditors.filter(editor => { return editor.document.uri.toString() === uri.toString(); }); - if(workspace.getConfiguration('vscoq.proof.cursor').sticky === true && - workspace.getConfiguration('vscoq.proof').mode === 0) { + if(workspace.getConfiguration('vscoq.proof.cursor').sticky === true || + workspace.getConfiguration('vscoq.proof').mode === 1) { editors.map(editor => { editor.selections = [new Selection(range.end, range.end)]; editor.revealRange(range, TextEditorRevealType.Default); diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 04c42865f..d550b79d2 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -201,6 +201,28 @@ let interpret_to_position st pos = | None -> (st, []) (* document is empty *) | Some id -> interpret_to st id +let get_next_range st pos = + match id_of_pos st pos with + | None -> None + | Some id -> + match Document.get_sentence st.document id with + | None -> None + | Some { stop } -> + match Document.find_sentence_after st.document (stop+1) with + | None -> Some (Document.range_of_id st.document id) + | Some { id } -> Some (Document.range_of_id st.document id) + +let get_previous_range st pos = + match id_of_pos st pos with + | None -> None + | Some id -> + match Document.get_sentence st.document id with + | None -> None + | Some { start } -> + match Document.find_sentence_before st.document (start) with + | None -> Some (Document.range_of_id st.document id) + | Some { id } -> Some (Document.range_of_id st.document id) + let interpret_to_previous st = match st.observe_id with | None -> failwith "interpret to previous with no observe_id" diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli index 9ccd92aa8..8466b3394 100644 --- a/language-server/dm/documentManager.mli +++ b/language-server/dm/documentManager.mli @@ -48,6 +48,12 @@ val clear_observe_id : state -> state val reset_to_top : state -> state (** [reset_to_top state] updates the state to make the observe_id Top *) +val get_next_range : state -> Position.t -> Range.t option +(** [get_next_range st pos] get the range of the next sentence relative to pos *) + +val get_previous_range : state -> Position.t -> Range.t option +(** [get_previous_pos st pos] get the range of the previous sentence relative to pos *) + val interpret_to_position : state -> Position.t -> (state * events) (** [interpret_to_position stateful doc pos] navigates to the last sentence ending before or at [pos] and returns the resulting state. The [stateful] flag diff --git a/language-server/protocol/extProtocol.ml b/language-server/protocol/extProtocol.ml index b14f9a3be..c9ad09160 100644 --- a/language-server/protocol/extProtocol.ml +++ b/language-server/protocol/extProtocol.ml @@ -40,6 +40,7 @@ module Notification = struct type t = { textDocument : VersionedTextDocumentIdentifier.t; + position: Position.t option; } [@@deriving yojson] end @@ -48,6 +49,7 @@ 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 dca3e06a4..c25dd1760 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -311,34 +311,50 @@ let coqtopInterpretToPoint params = sel_events @ [ mk_proof_view_event uri (Some position)] let coqtopStepBackward params = - let Notification.Client.StepBackwardParams.{ textDocument = { uri } } = params in + let Notification.Client.StepBackwardParams.{ textDocument = { uri }; position } = params in match Hashtbl.find_opt states (DocumentUri.to_path uri) with - | None -> log "[stepForward] ignoring event on non existant document"; [] + | None -> log "[stepBackward] ignoring event on non existant document"; [] | Some st -> - let (st, events) = Dm.DocumentManager.interpret_to_previous st in - let range = Dm.DocumentManager.observe_id_range st in - Hashtbl.replace states (DocumentUri.to_path uri) st; - update_view uri st; - match range with - | None -> - inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] - | Some range -> - [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + if !check_mode = Settings.Mode.Continuous then + match position with + | None -> [] + | Some pos -> + match Dm.DocumentManager.get_previous_range st pos with + | None -> [] + | Some range -> [mk_move_cursor_event uri range] + else + let (st, events) = Dm.DocumentManager.interpret_to_previous st in + let range = Dm.DocumentManager.observe_id_range st in + Hashtbl.replace states (DocumentUri.to_path uri) st; + update_view uri st; + match range with + | None -> + inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + | Some range -> + [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] let coqtopStepForward params = - let Notification.Client.StepForwardParams.{ textDocument = { uri } } = params in + let Notification.Client.StepForwardParams.{ textDocument = { uri }; position } = params in match Hashtbl.find_opt states (DocumentUri.to_path uri) with - | None -> log "[stepBackward] ignoring event on non existant document"; [] + | None -> log "[stepForward] ignoring event on non existant document"; [] | Some st -> - let (st, events) = Dm.DocumentManager.interpret_to_next st in - let range = Dm.DocumentManager.observe_id_range st in - Hashtbl.replace states (DocumentUri.to_path uri) st; - update_view uri st; - match range with - | None -> - inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] - | Some range -> - [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + if !check_mode = Settings.Mode.Continuous then + match position with + | None -> [] + | Some pos -> + match Dm.DocumentManager.get_next_range st pos with + | None -> [] + | Some range -> [mk_move_cursor_event uri range] + else + let (st, events) = Dm.DocumentManager.interpret_to_next st in + let range = Dm.DocumentManager.observe_id_range st in + Hashtbl.replace states (DocumentUri.to_path uri) st; + update_view uri st; + match range with + | None -> + inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + | Some range -> + [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] let make_CompletionItem i item : CompletionItem.t = let (label, insertText, typ, path) = Dm.CompletionItems.pp_completion_item item in