From 35c3472ce8e2edf60131a3f1f05207b0f19b8cb5 Mon Sep 17 00:00:00 2001
From: Will Thomas <30wthomas@gmail.com>
Date: Mon, 9 Sep 2024 09:36:20 -0500
Subject: [PATCH 1/4] Making vscoqtop compute next position from cursor
 position and adding server option for exact cursor position or next command

---
 README.md                               |  1 +
 client/package.json                     | 14 +++++++
 client/src/manualChecking.ts            | 10 ++++-
 language-server/dm/documentManager.ml   |  5 +++
 language-server/dm/documentManager.mli  |  3 ++
 language-server/dm/rawDocument.ml       | 20 ++++++++++
 language-server/dm/rawDocument.mli      |  1 +
 language-server/protocol/extProtocol.ml | 13 +++++++
 language-server/vscoqtop/lspManager.ml  | 52 ++++++++++++++++++-------
 9 files changed, 102 insertions(+), 17 deletions(-)

diff --git a/README.md b/README.md
index 7c01bc68d..860bf04a5 100644
--- a/README.md
+++ b/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
diff --git a/client/package.json b/client/package.json
index 2c0a950d7..ab980d3f3 100644
--- a/client/package.json
+++ b/client/package.json
@@ -177,6 +177,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",
diff --git a/client/src/manualChecking.ts b/client/src/manualChecking.ts
index 50f37f226..128b85d9a 100644
--- a/client/src/manualChecking.ts
+++ b/client/src/manualChecking.ts
@@ -1,6 +1,7 @@
 import {
     TextEditor,
-    commands
+    commands,
+    workspace
 } from 'vscode';
 
 import {
@@ -16,7 +17,12 @@ import { makeVersionedDocumentId } from './utilities/utils';
 export const sendInterpretToPoint = (editor: TextEditor,  client: Client) => {
     const textDocument = makeVersionedDocumentId(editor);
     const position = editor.selection.active;
-    client.sendNotification("vscoq/interpretToPoint", {textDocument: textDocument, position: position});
+    const mode = workspace.getConfiguration("vscoq.proof").pointInterpretationMode;
+    if(mode === 0) {
+        client.sendNotification("vscoq/interpretToPoint", {textDocument: textDocument, position: position});
+    } else {
+        client.sendNotification("vscoq/interpretToNextPoint", {textDocument: textDocument, position: position});
+    }
 };
 
 export const sendInterpretToEnd = (editor: TextEditor,  client: Client) => {
diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index e21913f46..1d1b6e42d 100644
--- a/language-server/dm/documentManager.ml
+++ b/language-server/dm/documentManager.ml
@@ -238,6 +238,11 @@ let get_messages st pos =
     | Some (_oloc,msg) -> (DiagnosticSeverity.Error, pp_of_coqpp msg) :: feedback
     | None -> feedback
 
+let get_position_of_next_sentence st start_pos =
+  let raw_doc = Document.raw_document st.document in
+  RawDocument.position_of_loc raw_doc @@
+  RawDocument.loc_of_next_position raw_doc start_pos
+
 let get_info_messages st pos =
   match id_of_pos_opt st pos with
   | None -> log "get_messages: Could not find id";[]
diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli
index 8a22d73e9..7143dfa2a 100644
--- a/language-server/dm/documentManager.mli
+++ b/language-server/dm/documentManager.mli
@@ -96,6 +96,9 @@ val get_messages : state -> Position.t option -> (DiagnosticSeverity.t * pp) lis
 val get_info_messages : state -> Position.t option -> (DiagnosticSeverity.t * pp) list
 (** returns the Feedback.Info level messages associated to a given position *)
 
+val get_position_of_next_sentence : state -> Position.t -> Position.t
+(** returns the position of the next sentence *)
+
 val get_document_symbols : state -> DocumentSymbol.t list
 
 val all_diagnostics : state -> Diagnostic.t list
diff --git a/language-server/dm/rawDocument.ml b/language-server/dm/rawDocument.ml
index cdb3732ff..0c79a1e96 100644
--- a/language-server/dm/rawDocument.ml
+++ b/language-server/dm/rawDocument.ml
@@ -77,6 +77,26 @@ let loc_of_position raw Position.{ line; character } =
   let charloc = get_character_loc linestr character in
   raw.lines.(line) + charloc
 
+let loc_of_next_position raw Position.{ line; character } =
+  let file_text = raw.text in
+  let linestr = line_text raw line in
+  let charloc = get_character_loc linestr character in
+  let curInd = raw.lines.(line) + charloc in
+  (* Search backwards until we find non-whitespace char *)
+  let first_non_whitespace_ind = Str.search_backward (Str.regexp "[^ \t\n\r]") file_text curInd in
+  let command_regex = Str.regexp "[-.{}*+]" in
+  (* Search forward until we find a command delimiting char *)
+  let command_ind = Str.search_forward command_regex file_text first_non_whitespace_ind in
+  if ((command_ind + 3 < String.length file_text) && (String.sub file_text command_ind 3) = "...") then
+    command_ind + 3
+  else
+    (* Now search forward until the end of a possible repeatable 
+      command delimiter
+    *)
+    let repeatable_regex = Str.regexp "[^*+-]" in
+    let repeatable_ind = Str.search_forward repeatable_regex file_text command_ind in
+    repeatable_ind + 1
+
 let end_loc raw =
   String.length raw.text
 
diff --git a/language-server/dm/rawDocument.mli b/language-server/dm/rawDocument.mli
index 9ab8b74cf..f10891a09 100644
--- a/language-server/dm/rawDocument.mli
+++ b/language-server/dm/rawDocument.mli
@@ -22,6 +22,7 @@ val text : t -> string
 
 val position_of_loc : t -> int -> Position.t
 val loc_of_position : t -> Position.t -> int
+val loc_of_next_position : t -> Position.t -> int
 val end_loc : t -> int
 
 val range_of_loc : t -> Loc.t -> Range.t
diff --git a/language-server/protocol/extProtocol.ml b/language-server/protocol/extProtocol.ml
index 840313f28..32c03bb1a 100644
--- a/language-server/protocol/extProtocol.ml
+++ b/language-server/protocol/extProtocol.ml
@@ -30,6 +30,15 @@ module Notification = struct
 
     end
 
+    module InterpretToNextPointParams = struct
+
+      type t = {
+        textDocument : VersionedTextDocumentIdentifier.t;
+        position : Position.t;
+      } [@@deriving yojson]
+
+    end
+
     module InterpretToEndParams = struct
 
       type t = {
@@ -60,6 +69,7 @@ module Notification = struct
     | Std of Lsp.Client_notification.t
     | InterpretToEnd of InterpretToEndParams.t
     | InterpretToPoint of InterpretToPointParams.t
+    | InterpretToNextPoint of InterpretToNextPointParams.t
     | StepForward of StepForwardParams.t
     | StepBackward of StepBackwardParams.t
 
@@ -69,6 +79,9 @@ module Notification = struct
       | "vscoq/interpretToPoint" ->
         let+ params = Lsp.Import.Json.message_params params InterpretToPointParams.t_of_yojson in
         InterpretToPoint params
+      | "vscoq/interpretToNextPoint" ->
+        let+ params = Lsp.Import.Json.message_params params InterpretToNextPointParams.t_of_yojson in
+        InterpretToNextPoint params
       | "vscoq/stepBackward" ->
         let+ params = Lsp.Import.Json.message_params params StepBackwardParams.t_of_yojson in
         StepBackward params
diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
index 8aa1db751..7c958162e 100644
--- a/language-server/vscoqtop/lspManager.ml
+++ b/language-server/vscoqtop/lspManager.ml
@@ -357,7 +357,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,7 +382,7 @@ 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
     replace_state (DocumentUri.to_path uri) st visible;
@@ -397,10 +397,31 @@ let coqtopInterpretToPoint params =
       else
         sel_events @ [mk_proof_view_event uri (Some error_range.end_)]
  
+let coqtopInterpretToNextPoint params =
+  let Notification.Client.InterpretToNextPointParams.{ textDocument; position } = params in
+  let uri = textDocument.uri in
+  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
+  | None -> log @@ "[interpretToNextPoint] ignoring event on non existent document"; []
+  | Some { st; visible } ->
+    let next_pos = Dm.DocumentManager.get_position_of_next_sentence st position in
+    let (st, events, error_range) = Dm.DocumentManager.interpret_to_position st next_pos ~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
+    match error_range with
+    | None ->
+      sel_events @ [ mk_proof_view_event uri (Some next_pos)]
+    | Some {last_range; error_range} ->
+      if !check_mode = Settings.Mode.Manual then
+        sel_events @ mk_block_on_error_event uri last_range error_range
+      else
+        sel_events @ [mk_proof_view_event uri (Some error_range.end_)]
+  
+
 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 +444,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 +484,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,7 +497,7 @@ 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)), []
@@ -484,7 +505,7 @@ let documentSymbol id params =
 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 +522,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 +536,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 +575,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 }, []
 
@@ -615,6 +636,7 @@ let dispatch_std_notification =
 let dispatch_notification =
   let open Notification.Client in function
   | InterpretToPoint params -> log "Received notification: vscoq/interpretToPoint"; coqtopInterpretToPoint params 
+  | InterpretToNextPoint params -> log "Received notification: vscoq/interpretToNextPoint"; coqtopInterpretToNextPoint params
   | InterpretToEnd params -> log "Received notification: vscoq/interpretToEnd"; coqtopInterpretToEnd params
   | StepBackward params -> log "Received notification: vscoq/stepBackward"; coqtopStepBackward params
   | StepForward params -> log "Received notification: vscoq/stepForward"; coqtopStepForward params
@@ -702,7 +724,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

From 0ab92c467252b34dd8d3f0956d4bf15b9ca1feb5 Mon Sep 17 00:00:00 2001
From: Will Thomas <30wthomas@gmail.com>
Date: Wed, 11 Sep 2024 22:11:31 -0500
Subject: [PATCH 2/4] updating interpret to point to take boolean next_point
 flag and use parsed document structures instead of regex

---
 client/src/manualChecking.ts            |  8 ++-----
 language-server/dm/documentManager.ml   | 27 +++++++++++++++++----
 language-server/dm/documentManager.mli  | 12 +++++-----
 language-server/dm/rawDocument.ml       | 20 ----------------
 language-server/dm/rawDocument.mli      |  1 -
 language-server/protocol/extProtocol.ml | 14 +----------
 language-server/vscoqtop/lspManager.ml  | 32 +++++++------------------
 7 files changed, 39 insertions(+), 75 deletions(-)

diff --git a/client/src/manualChecking.ts b/client/src/manualChecking.ts
index 128b85d9a..5ac79f4d0 100644
--- a/client/src/manualChecking.ts
+++ b/client/src/manualChecking.ts
@@ -14,15 +14,11 @@ 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;
     const mode = workspace.getConfiguration("vscoq.proof").pointInterpretationMode;
-    if(mode === 0) {
-        client.sendNotification("vscoq/interpretToPoint", {textDocument: textDocument, position: position});
-    } else {
-        client.sendNotification("vscoq/interpretToNextPoint", {textDocument: textDocument, position: position});
-    }
+    client.sendNotification("vscoq/interpretToPoint", {textDocument: textDocument, position: position, to_next_point: mode === 1 });
 };
 
 export const sendInterpretToEnd = (editor: TextEditor,  client: Client) => {
diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index 1d1b6e42d..7c05e4cd1 100644
--- a/language-server/dm/documentManager.ml
+++ b/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 before 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
@@ -238,11 +252,6 @@ let get_messages st pos =
     | Some (_oloc,msg) -> (DiagnosticSeverity.Error, pp_of_coqpp msg) :: feedback
     | None -> feedback
 
-let get_position_of_next_sentence st start_pos =
-  let raw_doc = Document.raw_document st.document in
-  RawDocument.position_of_loc raw_doc @@
-  RawDocument.loc_of_next_position raw_doc start_pos
-
 let get_info_messages st pos =
   match id_of_pos_opt st pos with
   | None -> log "get_messages: Could not find id";[]
@@ -323,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
diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli
index 7143dfa2a..179d0f5d8 100644
--- a/language-server/dm/documentManager.mli
+++ b/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]
@@ -96,9 +99,6 @@ val get_messages : state -> Position.t option -> (DiagnosticSeverity.t * pp) lis
 val get_info_messages : state -> Position.t option -> (DiagnosticSeverity.t * pp) list
 (** returns the Feedback.Info level messages associated to a given position *)
 
-val get_position_of_next_sentence : state -> Position.t -> Position.t
-(** returns the position of the next sentence *)
-
 val get_document_symbols : state -> DocumentSymbol.t list
 
 val all_diagnostics : state -> Diagnostic.t list
diff --git a/language-server/dm/rawDocument.ml b/language-server/dm/rawDocument.ml
index 0c79a1e96..cdb3732ff 100644
--- a/language-server/dm/rawDocument.ml
+++ b/language-server/dm/rawDocument.ml
@@ -77,26 +77,6 @@ let loc_of_position raw Position.{ line; character } =
   let charloc = get_character_loc linestr character in
   raw.lines.(line) + charloc
 
-let loc_of_next_position raw Position.{ line; character } =
-  let file_text = raw.text in
-  let linestr = line_text raw line in
-  let charloc = get_character_loc linestr character in
-  let curInd = raw.lines.(line) + charloc in
-  (* Search backwards until we find non-whitespace char *)
-  let first_non_whitespace_ind = Str.search_backward (Str.regexp "[^ \t\n\r]") file_text curInd in
-  let command_regex = Str.regexp "[-.{}*+]" in
-  (* Search forward until we find a command delimiting char *)
-  let command_ind = Str.search_forward command_regex file_text first_non_whitespace_ind in
-  if ((command_ind + 3 < String.length file_text) && (String.sub file_text command_ind 3) = "...") then
-    command_ind + 3
-  else
-    (* Now search forward until the end of a possible repeatable 
-      command delimiter
-    *)
-    let repeatable_regex = Str.regexp "[^*+-]" in
-    let repeatable_ind = Str.search_forward repeatable_regex file_text command_ind in
-    repeatable_ind + 1
-
 let end_loc raw =
   String.length raw.text
 
diff --git a/language-server/dm/rawDocument.mli b/language-server/dm/rawDocument.mli
index f10891a09..9ab8b74cf 100644
--- a/language-server/dm/rawDocument.mli
+++ b/language-server/dm/rawDocument.mli
@@ -22,7 +22,6 @@ val text : t -> string
 
 val position_of_loc : t -> int -> Position.t
 val loc_of_position : t -> Position.t -> int
-val loc_of_next_position : t -> Position.t -> int
 val end_loc : t -> int
 
 val range_of_loc : t -> Loc.t -> Range.t
diff --git a/language-server/protocol/extProtocol.ml b/language-server/protocol/extProtocol.ml
index 32c03bb1a..87660b9d4 100644
--- a/language-server/protocol/extProtocol.ml
+++ b/language-server/protocol/extProtocol.ml
@@ -26,15 +26,7 @@ module Notification = struct
       type t = {
         textDocument : VersionedTextDocumentIdentifier.t;
         position : Position.t;
-      } [@@deriving yojson]
-
-    end
-
-    module InterpretToNextPointParams = struct
-
-      type t = {
-        textDocument : VersionedTextDocumentIdentifier.t;
-        position : Position.t;
+        to_next_point : bool
       } [@@deriving yojson]
 
     end
@@ -69,7 +61,6 @@ module Notification = struct
     | Std of Lsp.Client_notification.t
     | InterpretToEnd of InterpretToEndParams.t
     | InterpretToPoint of InterpretToPointParams.t
-    | InterpretToNextPoint of InterpretToNextPointParams.t
     | StepForward of StepForwardParams.t
     | StepBackward of StepBackwardParams.t
 
@@ -79,9 +70,6 @@ module Notification = struct
       | "vscoq/interpretToPoint" ->
         let+ params = Lsp.Import.Json.message_params params InterpretToPointParams.t_of_yojson in
         InterpretToPoint params
-      | "vscoq/interpretToNextPoint" ->
-        let+ params = Lsp.Import.Json.message_params params InterpretToNextPointParams.t_of_yojson in
-        InterpretToNextPoint params
       | "vscoq/stepBackward" ->
         let+ params = Lsp.Import.Json.message_params params StepBackwardParams.t_of_yojson in
         StepBackward params
diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
index 7c958162e..1ad490801 100644
--- a/language-server/vscoqtop/lspManager.ml
+++ b/language-server/vscoqtop/lspManager.ml
@@ -379,12 +379,18 @@ let mk_block_on_error_event uri last_range error_range =
 
 
 let coqtopInterpretToPoint params =
-  let Notification.Client.InterpretToPointParams.{ textDocument; position } = params in
+  let Notification.Client.InterpretToPointParams.{ textDocument; position; to_next_point } = params in
   let uri = textDocument.uri in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
   | 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) =
+      if to_next_point
+      then Dm.DocumentManager.interpret_to_next_position st position ~should_block_on_error:!block_on_first_error
+      else 
+        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)
+    in
     replace_state (DocumentUri.to_path uri) st visible;
     update_view uri st;
     let sel_events = inject_dm_events (uri, events) in
@@ -397,27 +403,6 @@ let coqtopInterpretToPoint params =
       else
         sel_events @ [mk_proof_view_event uri (Some error_range.end_)]
  
-let coqtopInterpretToNextPoint params =
-  let Notification.Client.InterpretToNextPointParams.{ textDocument; position } = params in
-  let uri = textDocument.uri in
-  match Hashtbl.find_opt states (DocumentUri.to_path uri) with
-  | None -> log @@ "[interpretToNextPoint] ignoring event on non existent document"; []
-  | Some { st; visible } ->
-    let next_pos = Dm.DocumentManager.get_position_of_next_sentence st position in
-    let (st, events, error_range) = Dm.DocumentManager.interpret_to_position st next_pos ~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
-    match error_range with
-    | None ->
-      sel_events @ [ mk_proof_view_event uri (Some next_pos)]
-    | Some {last_range; error_range} ->
-      if !check_mode = Settings.Mode.Manual then
-        sel_events @ mk_block_on_error_event uri last_range error_range
-      else
-        sel_events @ [mk_proof_view_event uri (Some error_range.end_)]
-  
-
 let coqtopStepBackward params =
   let Notification.Client.StepBackwardParams.{ textDocument = { uri }; position } = params in
   match Hashtbl.find_opt states (DocumentUri.to_path uri) with
@@ -636,7 +621,6 @@ let dispatch_std_notification =
 let dispatch_notification =
   let open Notification.Client in function
   | InterpretToPoint params -> log "Received notification: vscoq/interpretToPoint"; coqtopInterpretToPoint params 
-  | InterpretToNextPoint params -> log "Received notification: vscoq/interpretToNextPoint"; coqtopInterpretToNextPoint params
   | InterpretToEnd params -> log "Received notification: vscoq/interpretToEnd"; coqtopInterpretToEnd params
   | StepBackward params -> log "Received notification: vscoq/stepBackward"; coqtopStepBackward params
   | StepForward params -> log "Received notification: vscoq/stepForward"; coqtopStepForward params

From 769a2e96706725c4d21e1a72806d04695ac6e261 Mon Sep 17 00:00:00 2001
From: Will Thomas <30wthomas@gmail.com>
Date: Wed, 11 Sep 2024 22:18:56 -0500
Subject: [PATCH 3/4] fixing typo in comment

---
 language-server/dm/documentManager.ml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
index 7c05e4cd1..207869c89 100644
--- a/language-server/dm/documentManager.ml
+++ b/language-server/dm/documentManager.ml
@@ -229,7 +229,7 @@ let id_of_sentence_after_pos st pos =
   match Document.find_sentence st.document loc with
   | Some { id } -> Some id
   | None -> 
-    (** otherwise the sentence start is before the loc,
+    (** 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
     *)

From dae58bad0033037ace50de10219fd58ee98ccfd3 Mon Sep 17 00:00:00 2001
From: Will Thomas <30wthomas@gmail.com>
Date: Fri, 13 Sep 2024 09:22:22 -0500
Subject: [PATCH 4/4] updating to make server option rather than passed per
 request

---
 client/src/manualChecking.ts            |  3 +--
 language-server/protocol/extProtocol.ml |  1 -
 language-server/protocol/settings.ml    | 17 +++++++++++++++++
 language-server/vscoqtop/lspManager.ml  | 14 +++++++++-----
 4 files changed, 27 insertions(+), 8 deletions(-)

diff --git a/client/src/manualChecking.ts b/client/src/manualChecking.ts
index 5ac79f4d0..efd0dda1b 100644
--- a/client/src/manualChecking.ts
+++ b/client/src/manualChecking.ts
@@ -17,8 +17,7 @@ import { makeVersionedDocumentId } from './utilities/utils';
 export const sendInterpretToPoint = (editor: TextEditor, client: Client) => {
     const textDocument = makeVersionedDocumentId(editor);
     const position = editor.selection.active;
-    const mode = workspace.getConfiguration("vscoq.proof").pointInterpretationMode;
-    client.sendNotification("vscoq/interpretToPoint", {textDocument: textDocument, position: position, to_next_point: mode === 1 });
+    client.sendNotification("vscoq/interpretToPoint", {textDocument: textDocument, position: position });
 };
 
 export const sendInterpretToEnd = (editor: TextEditor,  client: Client) => {
diff --git a/language-server/protocol/extProtocol.ml b/language-server/protocol/extProtocol.ml
index 87660b9d4..840313f28 100644
--- a/language-server/protocol/extProtocol.ml
+++ b/language-server/protocol/extProtocol.ml
@@ -26,7 +26,6 @@ module Notification = struct
       type t = {
         textDocument : VersionedTextDocumentIdentifier.t;
         position : Position.t;
-        to_next_point : bool
       } [@@deriving yojson]
 
     end
diff --git a/language-server/protocol/settings.ml b/language-server/protocol/settings.ml
index 860aa87cc..8fba19267 100644
--- a/language-server/protocol/settings.ml
+++ b/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
diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml
index 1ad490801..26bd4c144 100644
--- a/language-server/vscoqtop/lspManager.ml
+++ b/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
@@ -379,17 +382,18 @@ let mk_block_on_error_event uri last_range error_range =
 
 
 let coqtopInterpretToPoint params =
-  let Notification.Client.InterpretToPointParams.{ textDocument; position; to_next_point } = params in
+  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 existent document"; []
   | Some { st; visible } ->
     let (st, events, error_range, position) =
-      if to_next_point
-      then Dm.DocumentManager.interpret_to_next_position st position ~should_block_on_error:!block_on_first_error
-      else 
+      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;