From 5a36cc5b7e5e959caf6c08229536875bba416391 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Tue, 1 Aug 2023 17:06:21 +0200 Subject: [PATCH 1/4] Sticky cursor first draft: - Added the sticky cursor option in the package.json file - Tried using the updateHighlights notification to update the cursor to no avail - TODO: Will need to create a custom notification type --- client/package.json | 6 ++++++ client/src/extension.ts | 25 +++++++++++++++++++++---- client/src/protocol/types.ts | 9 ++++++++- 3 files changed, 35 insertions(+), 5 deletions(-) diff --git a/client/package.json b/client/package.json index f34b7e51..b5114fad 100644 --- a/client/package.json +++ b/client/package.json @@ -128,6 +128,12 @@ "default": 1, "description": "Configures the proof checking mode for Coq." }, + "vscoq.proof.cursor.sticky": { + "scope": "window", + "type": "boolean", + "default": true, + "description": "Move the editor's cursor position as Coq interactively steps forward/backward a command" + }, "vscoq.proof.delegation": { "scope": "window", "type": "string", diff --git a/client/src/extension.ts b/client/src/extension.ts index de285e1e..ebaac098 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -2,7 +2,9 @@ import {workspace, window, commands, ExtensionContext, TextEditorSelectionChangeEvent, TextEditorSelectionChangeKind, TextEditor, - ViewColumn, + ViewColumn, + TextEditorRevealType, + Selection, } from 'vscode'; import { @@ -16,7 +18,7 @@ import { checkVersion } from './utilities/versioning'; import {initializeDecorations} from './Decorations'; import GoalPanel from './panels/GoalPanel'; import SearchViewProvider from './panels/SearchViewProvider'; -import { ProofViewNotification, SearchCoqResult } from './protocol/types'; +import { ProofViewNotification, SearchCoqResult, UpdateHightlightsNotification } from './protocol/types'; import { sendInterpretToPoint, sendInterpretToEnd, @@ -121,9 +123,24 @@ export function activate(context: ExtensionContext) { // I think vscode should handle this automatically, TODO: try again after implemeting client capabilities context.subscriptions.push(workspace.onDidChangeConfiguration(event => updateServerOnConfigurationChange(event, context, client))); - client.onNotification("vscoq/updateHighlights", ({uri, parsedRange, processingRange, processedRange}) => { - client.saveHighlights(uri, parsedRange, processingRange, processedRange); + client.onNotification("vscoq/updateHighlights", (notification) => { + + client.saveHighlights( + notification.uri, + notification.parsedRange, + notification.processingRange, + notification.processedRange + ); + client.updateHightlights(); + + if(workspace.getConfiguration('vscoq.proof.cursor').sticky === true && + workspace.getConfiguration('vscoq.proof').mode === 0) { + const range = notification.processedRange[notification.processedRange.length - 1]; + const editor = window.activeTextEditor ? window.activeTextEditor : window.visibleTextEditors[0]; + editor.selections = [new Selection(range.end, range.end)]; + editor.revealRange(range, TextEditorRevealType.Default); + } }); client.onNotification("vscoq/searchResult", (searchResult: SearchCoqResult) => { diff --git a/client/src/protocol/types.ts b/client/src/protocol/types.ts index 2117e5f5..36ec418f 100644 --- a/client/src/protocol/types.ts +++ b/client/src/protocol/types.ts @@ -1,5 +1,5 @@ import { integer, TextDocumentIdentifier, VersionedTextDocumentIdentifier } from "vscode-languageclient"; -import { Position } from "vscode"; +import { Position, Range, Uri } from "vscode"; type Nullable = T | null; @@ -19,6 +19,13 @@ interface ProofViewNotificationType { givenUpGoals: Goal[]; } +export interface UpdateHightlightsNotification { + uri: Uri; + parsedRange: Range[]; + processingRange: Range[]; + processedRange: Range[]; +} + export type ProofViewNotification = Nullable; export interface SearchCoqRequest { From e2e15dcbc43fd1d38253921b502f120d0dfd327e Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Wed, 2 Aug 2023 11:36:56 +0200 Subject: [PATCH 2/4] Sticky cursor backend. In the language server: - Added a MoveCursor notification type - Added a function to get the last executed range in the DocumentManager - Added all functions and processes to launch the notification on a stepForward or stepBackward --- language-server/dm/documentManager.ml | 10 ++++++++ language-server/dm/documentManager.mli | 3 +++ language-server/lsp/extProtocol.ml | 14 +++++++++++ language-server/vscoqtop/lspManager.ml | 34 +++++++++++++++++++++++--- 4 files changed, 58 insertions(+), 3 deletions(-) diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index c776a105..965e22f9 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -98,6 +98,16 @@ let executed_ranges st = in executed_ranges st.document st.execution_state loc +let last_executed_range st = + let doc = Document.raw_document st.document in + match Option.bind st.observe_id (Document.get_sentence st.document) with + | None -> None + | Some { start; stop} -> + let start = RawDocument.position_of_loc doc start in + let end_ = RawDocument.position_of_loc doc stop in + let range = Range.{ start; end_ } in + Some range + let make_diagnostic doc range oloc message severity = let range = match oloc with diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli index 45c2d5be..729896ed 100644 --- a/language-server/dm/documentManager.mli +++ b/language-server/dm/documentManager.mli @@ -77,6 +77,9 @@ val executed_ranges : state -> exec_overview (** returns the ranges corresponding to the sentences that have been executed and remotely executes *) +val last_executed_range : state -> Lsp.LspData.Range.t option +(** returns the last executed sentence as a range **) + val diagnostics : state -> Diagnostic.t list (** diagnostics [doc] returns the diagnostics corresponding to the sentences that have been executed in [doc]. *) diff --git a/language-server/lsp/extProtocol.ml b/language-server/lsp/extProtocol.ml index dbc2eefd..0de95834 100644 --- a/language-server/lsp/extProtocol.ml +++ b/language-server/lsp/extProtocol.ml @@ -84,6 +84,15 @@ module Notification = struct end + module MoveCursorParams = struct + + type t = { + uri: Uri.t; + range: Range.t; + } [@@deriving yojson] + + end + module ProofViewParams = struct type t = ProofState.t option @@ -96,6 +105,7 @@ module Notification = struct type t = | Std of Protocol.Notification.Server.t | UpdateHighlights of UpdateHighlightsParams.t + | MoveCursor of MoveCursorParams.t | ProofView of ProofViewParams.t | SearchResult of query_result @@ -114,6 +124,10 @@ module Notification = struct let method_ = "vscoq/searchResult" in let params = yojson_of_query_result params in JsonRpc.Notification.{ method_; params } + | MoveCursor params -> + let method_ = "vscoq/moveCursor" in + let params = MoveCursorParams.yojson_of_t params in + JsonRpc.Notification.{ method_; params } end diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index 9cf0fd49..6161b471 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -51,6 +51,7 @@ type event = | Notification of notification | LogEvent of Dm.Log.event | SendProofView of Uri.t * Position.t option + | SendMoveCursor of Uri.t * Range.t type events = event Sel.event list @@ -185,6 +186,10 @@ let send_proof_view pv = let notification = Notification.Server.ProofView pv in output_jsonrpc @@ Notification Notification.Server.(jsonrpc_of_t notification) +let send_move_cursor uri range = + let notification = Notification.Server.MoveCursor {uri;range} in + output_jsonrpc @@ Notification Notification.Server.(jsonrpc_of_t notification) + let update_view uri st = if (Dm.ExecutionManager.is_diagnostics_enabled ()) then ( send_highlights uri st; @@ -252,6 +257,9 @@ let progress_hook uri () = let mk_proof_view_event uri position = Sel.set_priority Dm.PriorityManager.proof_view @@ Sel.now @@ SendProofView (uri, position) +let mk_move_cursor_event uri range = + Sel.set_priority Dm.PriorityManager.feedback @@ Sel.now @@ SendMoveCursor (uri, range) + let coqtopInterpretToPoint params = let Notification.Client.InterpretToPointParams.{ textDocument; position } = params in let uri = textDocument.uri in @@ -268,18 +276,34 @@ let coqtopStepBackward params = let st = Hashtbl.find states (Uri.path uri) in let st = Dm.DocumentManager.validate_document st in let (st, events) = Dm.DocumentManager.interpret_to_previous st in + let range = Dm.DocumentManager.last_executed_range st in Hashtbl.replace states (Uri.path uri) st; update_view uri st; - inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + if !check_mode = Settings.Mode.Manual then + match range with + | None -> + inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + | Some range -> + inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] @ [ mk_move_cursor_event uri range] + else + inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] let coqtopStepForward params = let Notification.Client.StepForwardParams.{ textDocument = { uri } } = params in let st = Hashtbl.find states (Uri.path uri) in let st = Dm.DocumentManager.validate_document st in let (st, events) = Dm.DocumentManager.interpret_to_next st in + let range = Dm.DocumentManager.last_executed_range st in Hashtbl.replace states (Uri.path uri) st; - update_view uri st; - inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + update_view uri st; + if !check_mode = Settings.Mode.Manual then + match range with + | None -> + inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] + | Some range -> + inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] @ [ mk_move_cursor_event uri range] + else + 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 @@ -476,6 +500,9 @@ let handle_event = function let st = Hashtbl.find states (Uri.path uri) in let pv = Dm.DocumentManager.get_proof st position in send_proof_view pv; [] + | SendMoveCursor (uri, range) -> + send_move_cursor uri range; [] + let pr_event = function | LspManagerEvent e -> pr_lsp_event e @@ -484,6 +511,7 @@ let pr_event = function | Notification _ -> Pp.str"notif" | LogEvent _ -> Pp.str"debug" | SendProofView _ -> Pp.str"proofview" + | SendMoveCursor _ -> Pp.str"move cursor" let init injections = init_state := Some (Vernacstate.freeze_full_state (), injections); From 3229486dc17bb3436a466808c1f31c9ad37c9472 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Wed, 2 Aug 2023 11:46:23 +0200 Subject: [PATCH 3/4] Sticky cursor frontend. In the vscode extension: - Added the mechanism to update the cursor on receiving a moveCursor notification. --- client/src/extension.ts | 22 ++++++++++++++-------- client/src/protocol/types.ts | 7 ++++++- 2 files changed, 20 insertions(+), 9 deletions(-) diff --git a/client/src/extension.ts b/client/src/extension.ts index ebaac098..99a4f1cf 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -18,7 +18,7 @@ import { checkVersion } from './utilities/versioning'; import {initializeDecorations} from './Decorations'; import GoalPanel from './panels/GoalPanel'; import SearchViewProvider from './panels/SearchViewProvider'; -import { ProofViewNotification, SearchCoqResult, UpdateHightlightsNotification } from './protocol/types'; +import { MoveCursorNotification, ProofViewNotification, SearchCoqResult, UpdateHightlightsNotification } from './protocol/types'; import { sendInterpretToPoint, sendInterpretToEnd, @@ -133,15 +133,21 @@ export function activate(context: ExtensionContext) { ); client.updateHightlights(); - + }); + + client.onNotification("vscoq/moveCursor", (notification: MoveCursorNotification) => { + const {uri, range} = notification; + 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) { - const range = notification.processedRange[notification.processedRange.length - 1]; - const editor = window.activeTextEditor ? window.activeTextEditor : window.visibleTextEditors[0]; - editor.selections = [new Selection(range.end, range.end)]; - editor.revealRange(range, TextEditorRevealType.Default); + workspace.getConfiguration('vscoq.proof').mode === 0) { + editors.map(editor => { + editor.selections = [new Selection(range.end, range.end)]; + editor.revealRange(range, TextEditorRevealType.Default); + }); } - }); + }); client.onNotification("vscoq/searchResult", (searchResult: SearchCoqResult) => { searchProvider.renderSearchResult(searchResult); diff --git a/client/src/protocol/types.ts b/client/src/protocol/types.ts index 36ec418f..3a2339f8 100644 --- a/client/src/protocol/types.ts +++ b/client/src/protocol/types.ts @@ -19,6 +19,8 @@ interface ProofViewNotificationType { givenUpGoals: Goal[]; } +export type ProofViewNotification = Nullable; + export interface UpdateHightlightsNotification { uri: Uri; parsedRange: Range[]; @@ -26,7 +28,10 @@ export interface UpdateHightlightsNotification { processedRange: Range[]; } -export type ProofViewNotification = Nullable; +export interface MoveCursorNotification { + uri: Uri; + range: Range; +} export interface SearchCoqRequest { id: string; From c0a1337c852d171007f29f66db85a5a482edc3b8 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Thu, 3 Aug 2023 09:51:01 +0200 Subject: [PATCH 4/4] Renaming and ammends: - Renamed the last_executed_range function to observe_id_range - Created a new pre_execution priority - Review priorities so that 1) we mve the cursor, 2) we execute, 3) we display the proof context --- language-server/dm/documentManager.ml | 2 +- language-server/dm/documentManager.mli | 4 ++-- language-server/dm/priorityManager.ml | 3 ++- language-server/vscoqtop/lspManager.ml | 10 +++++----- 4 files changed, 10 insertions(+), 9 deletions(-) diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 965e22f9..3371c991 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -98,7 +98,7 @@ let executed_ranges st = in executed_ranges st.document st.execution_state loc -let last_executed_range st = +let observe_id_range st = let doc = Document.raw_document st.document in match Option.bind st.observe_id (Document.get_sentence st.document) with | None -> None diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli index 729896ed..39f7447d 100644 --- a/language-server/dm/documentManager.mli +++ b/language-server/dm/documentManager.mli @@ -77,8 +77,8 @@ val executed_ranges : state -> exec_overview (** returns the ranges corresponding to the sentences that have been executed and remotely executes *) -val last_executed_range : state -> Lsp.LspData.Range.t option -(** returns the last executed sentence as a range **) +val observe_id_range : state -> Lsp.LspData.Range.t option +(** returns the range of the sentence referenced by observe_id **) val diagnostics : state -> Diagnostic.t list (** diagnostics [doc] returns the diagnostics corresponding to the sentences diff --git a/language-server/dm/priorityManager.ml b/language-server/dm/priorityManager.ml index 4f712d5f..e71064f2 100644 --- a/language-server/dm/priorityManager.ml +++ b/language-server/dm/priorityManager.ml @@ -3,4 +3,5 @@ let lsp_message = -3 let feedback = -2 let execution = -3 -let proof_view = -2 \ No newline at end of file +let proof_view = -2 +let pre_execution = -4 \ No newline at end of file diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index 6161b471..d0280bf8 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -258,7 +258,7 @@ let mk_proof_view_event uri position = Sel.set_priority Dm.PriorityManager.proof_view @@ Sel.now @@ SendProofView (uri, position) let mk_move_cursor_event uri range = - Sel.set_priority Dm.PriorityManager.feedback @@ Sel.now @@ SendMoveCursor (uri, range) + Sel.set_priority Dm.PriorityManager.pre_execution @@ Sel.now @@ SendMoveCursor (uri, range) let coqtopInterpretToPoint params = let Notification.Client.InterpretToPointParams.{ textDocument; position } = params in @@ -276,7 +276,7 @@ let coqtopStepBackward params = let st = Hashtbl.find states (Uri.path uri) in let st = Dm.DocumentManager.validate_document st in let (st, events) = Dm.DocumentManager.interpret_to_previous st in - let range = Dm.DocumentManager.last_executed_range st in + let range = Dm.DocumentManager.observe_id_range st in Hashtbl.replace states (Uri.path uri) st; update_view uri st; if !check_mode = Settings.Mode.Manual then @@ -284,7 +284,7 @@ let coqtopStepBackward params = | None -> inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] | Some range -> - inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] @ [ mk_move_cursor_event uri range] + [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] else inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] @@ -293,7 +293,7 @@ let coqtopStepForward params = let st = Hashtbl.find states (Uri.path uri) in let st = Dm.DocumentManager.validate_document st in let (st, events) = Dm.DocumentManager.interpret_to_next st in - let range = Dm.DocumentManager.last_executed_range st in + let range = Dm.DocumentManager.observe_id_range st in Hashtbl.replace states (Uri.path uri) st; update_view uri st; if !check_mode = Settings.Mode.Manual then @@ -301,7 +301,7 @@ let coqtopStepForward params = | None -> inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] | Some range -> - inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] @ [ mk_move_cursor_event uri range] + [ mk_move_cursor_event uri range] @ inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ] else inject_dm_events (uri,events) @ [ mk_proof_view_event uri None ]