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..99a4f1cf 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 { MoveCursorNotification, ProofViewNotification, SearchCoqResult, UpdateHightlightsNotification } from './protocol/types'; import { sendInterpretToPoint, sendInterpretToEnd, @@ -121,11 +123,32 @@ 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(); }); + 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) { + 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 2117e5f5..3a2339f8 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; @@ -21,6 +21,18 @@ interface ProofViewNotificationType { export type ProofViewNotification = Nullable; +export interface UpdateHightlightsNotification { + uri: Uri; + parsedRange: Range[]; + processingRange: Range[]; + processedRange: Range[]; +} + +export interface MoveCursorNotification { + uri: Uri; + range: Range; +} + export interface SearchCoqRequest { id: string; textDocument: VersionedTextDocumentIdentifier; diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index c776a105..3371c991 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 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 + | 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..39f7447d 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 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 that have been executed in [doc]. *) 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/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..d0280bf8 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.pre_execution @@ 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.observe_id_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 -> + [ 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 ] 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.observe_id_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 -> + [ 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 ] 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);