Merge pull request #532 from coq-community/enhance/sticky-cursor

Sticky cursor for step forward and step backward

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",

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);
         });

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> = T | null;
 
@@ -21,6 +21,18 @@ interface ProofViewNotificationType {
 
 export type ProofViewNotification = Nullable<ProofViewNotificationType>;
 
+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;

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

language-server/dm/documentManager.mli

@@ -72,6 +72,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]. *)

language-server/dm/priorityManager.ml

@@ -3,4 +3,5 @@
 let lsp_message = -3
 let feedback = -2
 let execution = -3
-let proof_view = -2
+let proof_view = -2
+let pre_execution = -4

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
 

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;
@@ -245,6 +250,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
@@ -259,17 +267,33 @@ let coqtopStepBackward params =
   let Notification.Client.StepBackwardParams.{ textDocument = { uri } } = params in
   let st = Hashtbl.find states (Uri.path uri) 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, 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
@@ -467,6 +491,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
@@ -475,6 +502,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);