Making vscoqtop compute next position from cursor position and server…

… option for exact cursor position or next command
coq · Sep 9, 2024 · 6191e97 · 6191e97
1 parent 6cc4d1d
commit 6191e97
Show file tree

Hide file tree

Showing 8 changed files with 147 additions and 85 deletions.
diff --git 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
@@ -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",
@@ -206,10 +220,10 @@
             "description": "Amount of workers assigned to proofs in delegation mode"
           },
           "vscoq.proof.block": {
-              "scope": "window",
-              "type": "boolean",
-              "default": true,
-              "description": "Should execution be halted after reaching the first error ? "
+            "scope": "window",
+            "type": "boolean",
+            "default": true,
+            "description": "Should execution be halted after reaching the first error ? "
           }
         }
       },
@@ -379,9 +393,9 @@
     "menus": {
       "editor/title": [
         {
-            "when": "resourceLangId == coq",
-            "command": "extension.coq.interpretToPoint",
-            "group": "navigation@3"
+          "when": "resourceLangId == coq",
+          "command": "extension.coq.interpretToPoint",
+          "group": "navigation@3"
         },
         {
           "when": "resourceLangId == coq",
@@ -414,7 +428,7 @@
           "group": "navigation@0"
         }
       ],
-      "vscoq.menu":[
+      "vscoq.menu": [
         {
           "when": "resourceLangId == coq",
           "command": "extension.coq.documentState",
@@ -436,14 +450,14 @@
           "group": "2_documentation@0"
         }
       ],
-      "vscoq.menu.doc":[
+      "vscoq.menu.doc": [
         {
-            "when": "resourceLangId == coq",
-            "command": "extension.coq.walkthrough"
+          "when": "resourceLangId == coq",
+          "command": "extension.coq.walkthrough"
         },
         {
-            "when": "resourceLangId == coq",
-            "command": "extension.coq.showManual"
+          "when": "resourceLangId == coq",
+          "command": "extension.coq.showManual"
         }
       ],
       "editor/context": [
@@ -859,46 +873,46 @@
       }
     ],
     "walkthroughs": [
-        {
-            "id": "coq.welcome",
-            "title": "Coq Setup",
-            "description": "Getting started with Coq",
-            "steps": [
-                {
-                    "id": "coq.welcome.openHelpPage",
-                    "title": "Re-open the setup page",
-                    "description": "This page is accessible at any moment by opening an empty file, clicking on the Coq menu and selecting ``Documentation > Docs: Show Setup Guide`` from the drop down menu.",
-                    "media": {
-                        "image": "./media/open_walkthrough.png",
-                        "altText": "Click on the Coq symbol and go to ```Docs: Show Setup Guide``` to re-open this walkthrough."
-                    }
-                },
-                {
-                    "id": "coq.welcome.books",
-                    "title": "Ressources to get started in the Coq world",
-                    "description": "You can find helpful books, documentations, and tutorials on this page",
-                    "media": {
-                        "markdown": "./media/books.md"
-                    }
-                },
-                {
-                    "id": "coq.welcome.install",
-                    "title": "Install dependencies",
-                    "description": "How to install Coq, setup VsCoq and its dependencies",
-                    "media": {
-                        "markdown": "./media/install.md"
-                    }
-                },
-                {
-                    "id": "coq.welcome.troubleshooting",
-                    "title": "Getting help",
-                    "description": "If you have any questions or are having problem with any of the previous steps, please head over to the [Coq zulip chat](https://coq.zulipchat.com/) so we can help you.",
-                    "media": {
-                        "markdown": "./media/troubleshooting.md"
-                    }
-                }
-            ]
-        }
+      {
+        "id": "coq.welcome",
+        "title": "Coq Setup",
+        "description": "Getting started with Coq",
+        "steps": [
+          {
+            "id": "coq.welcome.openHelpPage",
+            "title": "Re-open the setup page",
+            "description": "This page is accessible at any moment by opening an empty file, clicking on the Coq menu and selecting ``Documentation > Docs: Show Setup Guide`` from the drop down menu.",
+            "media": {
+              "image": "./media/open_walkthrough.png",
+              "altText": "Click on the Coq symbol and go to ```Docs: Show Setup Guide``` to re-open this walkthrough."
+            }
+          },
+          {
+            "id": "coq.welcome.books",
+            "title": "Ressources to get started in the Coq world",
+            "description": "You can find helpful books, documentations, and tutorials on this page",
+            "media": {
+              "markdown": "./media/books.md"
+            }
+          },
+          {
+            "id": "coq.welcome.install",
+            "title": "Install dependencies",
+            "description": "How to install Coq, setup VsCoq and its dependencies",
+            "media": {
+              "markdown": "./media/install.md"
+            }
+          },
+          {
+            "id": "coq.welcome.troubleshooting",
+            "title": "Getting help",
+            "description": "If you have any questions or are having problem with any of the previous steps, please head over to the [Coq zulip chat](https://coq.zulipchat.com/) so we can help you.",
+            "media": {
+              "markdown": "./media/troubleshooting.md"
+            }
+          }
+        ]
+      }
     ]
   },
   "scripts": {
@@ -943,4 +957,4 @@
     "webpack": "^5.94.0",
     "webpack-cli": "^5.0.0"
   }
-}
+}
diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml
@@ -217,18 +217,21 @@ let all_diagnostics st =
     List.map (mk_error_diag st) exec_errors @
     List.map (mk_diag st) feedback
 
-let id_of_pos st pos =
-  let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in
+let id_of_pos st pos ~next_pos =
+  let loc = 
+    if next_pos 
+    then RawDocument.loc_of_next_position (Document.raw_document st.document) pos 
+  else RawDocument.loc_of_position (Document.raw_document st.document) pos in
   match Document.find_sentence_before st.document loc with
   | None -> None
   | Some { id } -> Some id
 
-let id_of_pos_opt st = function
+let id_of_pos_opt st ~next_pos = 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
+  | Some pos -> id_of_pos st pos ~next_pos
 
-let get_messages st pos =
-  match id_of_pos_opt st pos with
+let get_messages st pos ~next_pos =
+  match id_of_pos_opt st pos ~next_pos with
   | None -> log "get_messages: Could not find id";[]
   | Some id -> log "get_messages: Found id";
     let error = ExecutionManager.error st.execution_state id in
@@ -238,8 +241,8 @@ let get_messages st pos =
     | Some (_oloc,msg) -> (DiagnosticSeverity.Error, pp_of_coqpp msg) :: feedback
     | None -> feedback
 
-let get_info_messages st pos =
-  match id_of_pos_opt st pos with
+let get_info_messages st pos ~next_pos =
+  match id_of_pos_opt st pos ~next_pos with
   | None -> log "get_messages: Could not find id";[]
   | Some id -> log "get_messages: Found id";
     let info (lvl, _, _, _) = 
@@ -313,13 +316,13 @@ let interpret_to st id ~should_block_on_error =
   let st = { st with observe_id} in
   observe ~background:false st id ~should_block_on_error
 
-let interpret_to_position st pos ~should_block_on_error =
-  match id_of_pos st pos with
+let interpret_to_position st pos ~should_block_on_error ~next_pos =
+  match id_of_pos st pos ~next_pos with
   | None -> (st, [], None) (* document is empty *)
   | Some id -> interpret_to st id ~should_block_on_error
 
-let get_next_range st pos =
-  match id_of_pos st pos with
+let get_next_range st pos ~next_pos =
+  match id_of_pos st pos ~next_pos with
   | None -> None
   | Some id ->
     match Document.get_sentence st.document id with
@@ -329,8 +332,8 @@ let get_next_range st pos =
       | None -> Some (Document.range_of_id st.document id)
       | Some { id } -> Some (Document.range_of_id st.document id)
 
-let get_previous_range st pos =
-  match id_of_pos st pos with
+let get_previous_range st pos ~next_pos =
+  match id_of_pos st pos ~next_pos with
   | None -> None
   | Some id ->
     match Document.get_sentence st.document id with
@@ -521,7 +524,7 @@ let handle_event ev st block =
   | ExecutionManagerEvent ev ->
     handle_execution_manager_event st ev
 
-let get_proof st diff_mode pos =
+let get_proof st diff_mode pos ~next_pos =
   let previous_st id =
     let oid = fst @@ Scheduler.task_for_sentence (Document.schedule st.document) id in
     Option.bind oid (ExecutionManager.get_vernac_state st.execution_state)
@@ -531,7 +534,7 @@ let get_proof st diff_mode pos =
     | None -> None
     | Some observe_id -> to_sentence_id observe_id 
   in
-  let oid = Option.cata (id_of_pos st) observe_id pos in
+  let oid = Option.cata (id_of_pos st ~next_pos) observe_id pos in
   let ost = Option.bind oid (ExecutionManager.get_vernac_state st.execution_state) in
   let previous = Option.bind oid previous_st in
   Option.bind ost (ProofState.get_proof ~previous diff_mode)
@@ -541,10 +544,10 @@ let context_of_id st = function
   | Some id -> ExecutionManager.get_context st.execution_state id
 
 (** Get context at the start of the sentence containing [pos] *)
-let get_context st pos = context_of_id st (id_of_pos st pos)
+let get_context st pos = context_of_id st (id_of_pos st pos ~next_pos:false)
 
 let get_completions st pos =
-  match id_of_pos st pos with
+  match id_of_pos st pos ~next_pos:false with
   | None -> Error ("Can't get completions, no sentence found before the cursor")
   | Some id ->
     let ost = ExecutionManager.get_vernac_state st.execution_state id in

diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli
@@ -53,13 +53,13 @@ val clear_observe_id : state -> state
 val reset_to_top : state -> state
 (** [reset_to_top state] updates the state to make the observe_id Top *)
 
-val get_next_range : state -> Position.t -> Range.t option
+val get_next_range : state -> Position.t -> next_pos:bool -> Range.t option
 (** [get_next_range st pos] get the range of the next sentence relative to pos *)
 
-val get_previous_range : state -> Position.t -> Range.t option
+val get_previous_range : state -> Position.t -> next_pos:bool -> 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)
+val interpret_to_position : state -> Position.t -> should_block_on_error:bool -> next_pos: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. *)
@@ -90,10 +90,10 @@ val executed_ranges : state -> exec_overview
 val observe_id_range : state -> Range.t option
 (** returns the range of the sentence referenced by observe_id **)
 
-val get_messages : state -> Position.t option -> (DiagnosticSeverity.t * pp) list
+val get_messages : state -> Position.t option -> next_pos:bool -> (DiagnosticSeverity.t * pp) list
 (** returns the messages associated to a given position *)
 
-val get_info_messages : state -> Position.t option -> (DiagnosticSeverity.t * pp) list
+val get_info_messages : state -> Position.t option -> next_pos:bool -> (DiagnosticSeverity.t * pp) list
 (** returns the Feedback.Info level messages associated to a given position *)
 
 val get_document_symbols : state -> DocumentSymbol.t list
@@ -102,7 +102,7 @@ val all_diagnostics : state -> Diagnostic.t list
 (** all_diagnostics [doc] returns the diagnostics corresponding to the sentences
     that have been executed in [doc]. *)
 
-val get_proof : state -> Settings.Goals.Diff.Mode.t -> Position.t option -> ProofState.t option
+val get_proof : state -> Settings.Goals.Diff.Mode.t -> Position.t option -> next_pos:bool -> ProofState.t option
 
 val get_completions : state -> Position.t -> (completion_item list, string) Result.t
 

diff --git 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
@@ -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/settings.ml b/language-server/protocol/settings.ml
@@ -60,11 +60,28 @@ module Memory = struct
 
 end
 
+module PointInterpMode = 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 Proof = struct
 
   type t = {
     delegation: DelegationMode.t;
     workers: int option;
+    pointInterpretationMode : PointInterpMode.t;
     mode: Mode.t;
     block: bool;
   } [@@deriving yojson] [@@yojson.allow_extra_fields]