Making vscoqtop compute next position from cursor position and adding…

… server option for exact cursor position or next command
coq · Sep 9, 2024 · f8b2c9f · f8b2c9f
1 parent 89e249d
commit f8b2c9f
Show file tree

Hide file tree

Showing 9 changed files with 156 additions and 71 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/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
@@ -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
@@ -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
@@ -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/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