Merge pull request #875 from Durbatuluk1701/cursor-nav-improvements

feat: adding option for interpreting to exact cursor position or next command during interpret to point

README.md

@@ -162,6 +162,7 @@ After installation and activation of the extension:
 
 #### Proof checking
 * `"vscoq.proof.mode": Continuous | Manual` -- Decide whether documents should checked continuously or using the classic navigation commmands (defaults to `Manual`)
+* `"vscoq.proof.pointInterpretationMode": Cursor | NextCommand` -- Determines the point to which the proof should be check to when using the 'Interpret to point' command. 
 * `"vscoq.proof.cursor.sticky": bool` -- a toggle to specify whether the cursor should move as Coq interactively navigates a document (step forward, backward, etc...)
 * `"vscoq.proof.delegation": None | Skip | Delegate` -- Decides which delegation strategy should be used by the server. 
   `Skip` allows to skip proofs which are out of focus and should be used in manual mode. `Delegate` allocates a settable amount of workers

client/package.json

@@ -199,6 +199,20 @@
             "default": 0,
             "description": "Configures the proof checking mode for Coq."
           },
+          "vscoq.proof.pointInterpretationMode": {
+            "scope": "window",
+            "type": "number",
+            "enum": [
+              0,
+              1
+            ],
+            "enumItemLabels": [
+              "Cursor",
+              "NextCommand"
+            ],
+            "default": 0,
+            "description": "Determines the point to which the proof should be checked when using the `Interpret to point` command."
+          },
           "vscoq.proof.cursor.sticky": {
             "scope": "window",
             "type": "boolean",

client/src/manualChecking.ts

@@ -1,6 +1,7 @@
 import {
     TextEditor,
-    commands
+    commands,
+    workspace
 } from 'vscode';
 
 import {
@@ -13,10 +14,10 @@ import GoalPanel from './panels/GoalPanel';
 import Client from './client';
 import { makeVersionedDocumentId } from './utilities/utils';
 
-export const sendInterpretToPoint = (editor: TextEditor,  client: Client) => {
+export const sendInterpretToPoint = (editor: TextEditor, client: Client) => {
     const textDocument = makeVersionedDocumentId(editor);
     const position = editor.selection.active;
-    client.sendNotification("vscoq/interpretToPoint", {textDocument: textDocument, position: position});
+    client.sendNotification("vscoq/interpretToPoint", {textDocument: textDocument, position: position });
 };
 
 export const sendInterpretToEnd = (editor: TextEditor,  client: Client) => {

language-server/dm/documentManager.ml

@@ -223,6 +223,20 @@ let id_of_pos st pos =
   | None -> None
   | Some { id } -> Some id
 
+let id_of_sentence_after_pos st pos =
+  let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
+  (* if the current loc falls squarely within a sentence *)
+  match Document.find_sentence st.document loc with
+  | Some { id } -> Some id
+  | None -> 
+    (** otherwise the sentence start is after the loc,
+        so we must be in the whitespace before the sentence
+        and need to interpret to the sentence before instead
+    *)
+    match Document.find_sentence_before st.document loc with
+    | None -> None
+    | Some { id } -> Some id
+
 let id_of_pos_opt st = function
   | None -> begin match st.observe_id with None | Some Top  -> None | Some Id id -> Some id end
   | Some pos -> id_of_pos st pos
@@ -318,6 +332,14 @@ let interpret_to_position st pos ~should_block_on_error =
   | None -> (st, [], None) (* document is empty *)
   | Some id -> interpret_to st id ~should_block_on_error
 
+let interpret_to_next_position st pos ~should_block_on_error =
+  match id_of_sentence_after_pos st pos with
+  | None -> (st, [], None, pos) (* document is empty *)
+  | Some id ->
+    let new_pos = (Document.range_of_id st.document id).end_ in
+    let (st, events, blocking_errs) = interpret_to st id ~should_block_on_error in
+    (st, events, blocking_errs, new_pos)
+
 let get_next_range st pos =
   match id_of_pos st pos with
   | None -> None

language-server/dm/documentManager.mli

@@ -60,9 +60,12 @@ 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 -> should_block_on_error:bool -> (state * events * blocking_error option)
-(** [interpret_to_position stateful doc pos] navigates to the last sentence ending
-    before or at [pos] and returns the resulting state. The [stateful] flag 
-    determines if we record the resulting position in the state. *)
+(** [interpret_to_position state pos should_block] navigates to the 
+    last sentence ending before or at [pos] and returns the resulting state, events that need to take place, and a possible blocking error. *)
+
+val interpret_to_next_position : state -> Position.t -> should_block_on_error:bool -> (state * events * blocking_error option * Position.t)
+(** [interpret_to_next_position state pos should_block] navigates 
+    to the first sentence after or at [pos] (excluding whitespace) and returns the resulting state, events that need to take place, a possible blocking error, and the position of the sentence that was interpreted until. *)
 
 val interpret_to_previous : state -> (state * events * blocking_error option)
 (** [interpret_to_previous doc] navigates to the previous sentence in [doc]

language-server/protocol/settings.ml

@@ -52,6 +52,22 @@ module Mode = struct
 
 end
 
+module PointInterpretationMode = struct
+  type t =
+  | Cursor
+  | NextCommand
+  [@@deriving yojson]
+
+  let yojson_of_t = function
+  | Cursor -> `Int 0
+  | NextCommand -> `Int 1
+
+  let t_of_yojson = function
+  | `Int 0 -> Cursor
+  | `Int 1 -> NextCommand
+  | _ -> Yojson.json_error @@ "invalid value "
+end
+
 module Memory = struct
 
   type t = {
@@ -67,6 +83,7 @@ module Proof = struct
     workers: int option;
     mode: Mode.t;
     block: bool;
+    pointInterpretationMode: PointInterpretationMode.t
   } [@@deriving yojson] [@@yojson.allow_extra_fields]
 
 end

language-server/vscoqtop/lspManager.ml

@@ -41,6 +41,8 @@ let max_memory_usage  = ref 4000000000
 let full_diagnostics = ref false
 let full_messages = ref false
 
+let point_interp_mode = ref Settings.PointInterpretationMode.Cursor
+
 let block_on_first_error = ref true
 
 let Dm.Types.Log log = Dm.Log.mk_log "lspManager"
@@ -130,7 +132,8 @@ let do_configuration settings =
   full_diagnostics := settings.diagnostics.full;
   full_messages := settings.goals.messages.full;
   max_memory_usage := settings.memory.limit * 1000000000;
-  block_on_first_error := settings.proof.block
+  block_on_first_error := settings.proof.block;
+  point_interp_mode := settings.proof.pointInterpretationMode
 
 let send_configuration_request () =
   let id = `Int conf_request_id in
@@ -357,7 +360,7 @@ let textDocumentHover id params =
 
 let progress_hook uri () =
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "ignoring non existant document"
+  | None -> log @@ "ignoring non existent document"
   | Some { st } -> update_view uri st
 
 let mk_proof_view_event uri position = 
@@ -382,9 +385,16 @@ let coqtopInterpretToPoint params =
   let Notification.Client.InterpretToPointParams.{ textDocument; position } = params in
   let uri = textDocument.uri in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "[interpretToPoint] ignoring event on non existant document"; []
+  | None -> log @@ "[interpretToPoint] ignoring event on non existent document"; []
   | Some { st; visible } ->
-    let (st, events, error_range) = Dm.DocumentManager.interpret_to_position st position ~should_block_on_error:!block_on_first_error in
+    let (st, events, error_range, position) =
+      match !point_interp_mode with
+      | Settings.PointInterpretationMode.Cursor ->
+        let st, evs, blocking_err = Dm.DocumentManager.interpret_to_position st position ~should_block_on_error:!block_on_first_error in
+        (st, evs, blocking_err, position)
+      | Settings.PointInterpretationMode.NextCommand ->
+        Dm.DocumentManager.interpret_to_next_position st position ~should_block_on_error:!block_on_first_error
+    in
     replace_state (DocumentUri.to_path uri) st visible;
     update_view uri st;
     let sel_events = inject_dm_events (uri, events) in
@@ -400,7 +410,7 @@ let coqtopInterpretToPoint params =
 let coqtopStepBackward params =
   let Notification.Client.StepBackwardParams.{ 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 "[stepBackward] ignoring event on non existent document"; []
   | Some { st; visible } ->
     if !check_mode = Settings.Mode.Continuous then
       match position with
@@ -423,7 +433,7 @@ let coqtopStepBackward params =
 let coqtopStepForward params =
   let Notification.Client.StepForwardParams.{ 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 "[stepForward] ignoring event on non existent document"; []
   | Some { st; visible } ->
     if !check_mode = Settings.Mode.Continuous then
       match position with
@@ -463,7 +473,7 @@ let textDocumentCompletion id params =
   else
   let Lsp.Types.CompletionParams.{ textDocument = { uri }; position } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "[textDocumentCompletion]ignoring event on non existant document"; Error("Document does not exist"), []
+  | None -> log @@ "[textDocumentCompletion]ignoring event on non existent document"; Error("Document does not exist"), []
   | Some { st } -> 
     match Dm.DocumentManager.get_completions st position with
     | Ok completionItems -> 
@@ -476,15 +486,15 @@ let textDocumentCompletion id params =
 let documentSymbol id params =
   let Lsp.Types.DocumentSymbolParams.{ textDocument = {uri}} = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "[documentSymbol] ignoring event on non existant document"; Error("Document does not exist"), []
+  | None -> log @@ "[documentSymbol] ignoring event on non existent document"; Error("Document does not exist"), []
   | Some tab -> log @@ "[documentSymbol] getting symbols";
     let symbols = Dm.DocumentManager.get_document_symbols tab.st in
     Ok(Some (`DocumentSymbol symbols)), []
 
 let coqtopResetCoq id params =
   let Request.Client.ResetParams.{ textDocument = { uri } } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "[resetCoq] ignoring event on non existant document"; Error("Document does not exist"), []
+  | None -> log @@ "[resetCoq] ignoring event on non existent document"; Error("Document does not exist"), []
   | Some { st; visible } -> 
     let st, events = Dm.DocumentManager.reset st in
     let (st, events') =
@@ -501,7 +511,7 @@ let coqtopResetCoq id params =
 let coqtopInterpretToEnd params =
   let Notification.Client.InterpretToEndParams.{ textDocument = { uri } } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "[interpretToEnd] ignoring event on non existant document"; []
+  | None -> log @@ "[interpretToEnd] ignoring event on non existent document"; []
   | Some { st; visible } ->
     let (st, events, error_range) = Dm.DocumentManager.interpret_to_end st ~should_block_on_error:!block_on_first_error in
     replace_state (DocumentUri.to_path uri) st visible;
@@ -515,32 +525,32 @@ let coqtopInterpretToEnd params =
 let coqtopLocate id params = 
   let Request.Client.LocateParams.{ textDocument = { uri }; position; pattern } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "[locate] ignoring event on non existant document"; Error("Document does not exist"), []
+  | None -> log @@ "[locate] ignoring event on non existent document"; Error("Document does not exist"), []
   | Some { st } ->
     Dm.DocumentManager.locate st position ~pattern, []
 
 let coqtopPrint id params = 
   let Request.Client.PrintParams.{ textDocument = { uri }; position; pattern } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "[print] ignoring event on non existant document"; Error("Document does not exist"), []
+  | None -> log @@ "[print] ignoring event on non existent document"; Error("Document does not exist"), []
   | Some { st } -> Dm.DocumentManager.print st position ~pattern, []
 
 let coqtopAbout id params =
   let Request.Client.AboutParams.{ textDocument = { uri }; position; pattern } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "[about] ignoring event on non existant document"; Error("Document does not exist"), []
+  | None -> log @@ "[about] ignoring event on non existent document"; Error("Document does not exist"), []
   | Some { st } -> Dm.DocumentManager.about st position ~pattern, []
 
 let coqtopCheck id params =
   let Request.Client.CheckParams.{ textDocument = { uri }; position; pattern } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "[check] ignoring event on non existant document"; Error("Document does not exist"), []
+  | None -> log @@ "[check] ignoring event on non existent document"; Error("Document does not exist"), []
   | Some { st } -> Dm.DocumentManager.check st position ~pattern, []
 
 let coqtopSearch id params =
   let Request.Client.SearchParams.{ textDocument = { uri }; id; position; pattern } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "[search] ignoring event on non existant document"; Error("Document does not exist"), []
+  | None -> log @@ "[search] ignoring event on non existent document"; Error("Document does not exist"), []
   | Some { st } ->
     try
       let notifications = Dm.DocumentManager.search st ~id position pattern in
@@ -554,7 +564,7 @@ let sendDocumentState id params =
   let Request.Client.DocumentStateParams.{ textDocument } = params in
   let uri = textDocument.uri in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "[documentState] ignoring event on non existant document"; Error("Document does not exist"), []
+  | None -> log @@ "[documentState] ignoring event on non existent document"; Error("Document does not exist"), []
   | Some { st } -> let document = Dm.DocumentManager.Internal.string_of_state st in
     Ok Request.Client.DocumentStateResult.{ document }, []
 
@@ -702,7 +712,7 @@ let handle_event = function
     send_coq_debug e; [inject_debug_event Dm.Log.debug]
   | SendProofView (uri, position) -> 
     begin match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-    | None -> log @@ "ignoring event on non existant document"; []
+    | None -> log @@ "ignoring event on non existent document"; []
     | Some { st } ->
       let proof = Dm.DocumentManager.get_proof st !diff_mode position in
       let messages = Dm.DocumentManager.get_messages st position in