diff --git a/README.md b/README.md index 81b6038b..8a259ce2 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 1ef50842..b079927a 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", @@ -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" } -} +} \ No newline at end of file diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 79c15280..6b0c9dcb 100644 --- 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 index 8a22d73e..9f7dd93d 100644 --- 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 index 290bb331..6a250326 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 9ab8b74c..f10891a0 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/settings.ml b/language-server/protocol/settings.ml index 860aa87c..e9bd14d6 100644 --- 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] diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index 8aa1db75..cfa69947 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -43,6 +43,8 @@ let full_messages = ref false let block_on_first_error = ref true +let interp_to_next_position = ref true + let Dm.Types.Log log = Dm.Log.mk_log "lspManager" let conf_request_id = max_int @@ -130,7 +132,11 @@ 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; + interp_to_next_position := + match settings.proof.pointInterpretationMode with + | Cursor -> false + | NextCommand -> true let send_configuration_request () = let id = `Int conf_request_id in @@ -384,7 +390,7 @@ let coqtopInterpretToPoint params = match Hashtbl.find_opt states (DocumentUri.to_path uri) with | None -> log @@ "[interpretToPoint] ignoring event on non existant 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) = Dm.DocumentManager.interpret_to_position st position ~should_block_on_error:!block_on_first_error ~next_pos:!interp_to_next_position in replace_state (DocumentUri.to_path uri) st visible; update_view uri st; let sel_events = inject_dm_events (uri, events) in @@ -406,7 +412,7 @@ let coqtopStepBackward params = match position with | None -> [] | Some pos -> - match Dm.DocumentManager.get_previous_range st pos with + match Dm.DocumentManager.get_previous_range st pos ~next_pos:!interp_to_next_position with | None -> [] | Some range -> [mk_move_cursor_event uri range] else @@ -429,7 +435,7 @@ let coqtopStepForward params = match position with | None -> [] | Some pos -> - match Dm.DocumentManager.get_next_range st pos with + match Dm.DocumentManager.get_next_range st pos ~next_pos:!interp_to_next_position with | None -> [] | Some range -> [mk_move_cursor_event uri range] else @@ -702,10 +708,10 @@ 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 + let proof = Dm.DocumentManager.get_proof st !diff_mode position ~next_pos:!interp_to_next_position in + let messages = Dm.DocumentManager.get_messages st position ~next_pos:!interp_to_next_position in let messages = if !full_messages then messages else List.filter (fun (sev,_) -> sev == DiagnosticSeverity.Information) messages