From 4f1a64773138969eeec640ea4ece89ca81996303 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Fri, 6 Dec 2024 10:52:41 +0100 Subject: [PATCH 01/10] feat: adding proof blocks to outline elements This will allow to create an api so that outside extensions can query the document and get a structured view of the proofs it contains. --- language-server/dm/document.ml | 30 ++++++++++++++++++++++++++++-- language-server/dm/document.mli | 9 ++++++++- language-server/dm/rawDocument.ml | 6 ++++++ language-server/dm/rawDocument.mli | 1 + 4 files changed, 43 insertions(+), 3 deletions(-) diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index 6d0e8caf..3c3570ee 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -27,11 +27,18 @@ type proof_block_type = | DefinitionType of Decls.definition_object_kind | Other +type proof_step = { + id: sentence_id; + tactic: string; + range: Range.t; +} + type outline_element = { id: sentence_id; name: string; type_: proof_block_type; statement: string; + proof: proof_step list; range: Range.t } @@ -132,11 +139,20 @@ let range_of_sentence raw (sentence : sentence) = let end_ = RawDocument.position_of_loc raw sentence.stop in Range.{ start; end_ } +let string_of_sentence raw (sentence: sentence) = + let string = RawDocument.string_in_range raw sentence.start sentence.stop in + string + let range_of_sentence_with_blank_space raw (sentence : sentence) = let start = RawDocument.position_of_loc raw sentence.parsing_start in let end_ = RawDocument.position_of_loc raw sentence.stop in Range.{ start; end_ } +let string_of_id document id = + match SM.find_opt id document.sentences_by_id with + | None -> CErrors.anomaly Pp.(str"Trying to get range of non-existing sentence " ++ Stateid.print id) + | Some sentence -> string_of_sentence document.raw_doc sentence + let range_of_id document id = match SM.find_opt id document.sentences_by_id with | None -> CErrors.anomaly Pp.(str"Trying to get range of non-existing sentence " ++ Stateid.print id) @@ -147,10 +163,20 @@ let range_of_id_with_blank_space document id = | None -> CErrors.anomaly Pp.(str"Trying to get range of non-existing sentence " ++ Stateid.print id) | Some sentence -> range_of_sentence_with_blank_space document.raw_doc sentence +let push_proof_step_in_outline document id (outline : outline) = + let range = range_of_id document id in + let tactic = string_of_id document id in + let proof_step = {id; tactic; range} in + match outline with + | [] -> outline + | e :: l -> + let proof = proof_step :: e.proof in + {e with proof} :: l let record_outline document id (ast : Synterp.vernac_control_entry) classif (outline : outline) = let open Vernacextend in match classif with + | VtProofStep _ -> push_proof_step_in_outline document id outline | VtStartProof (_, names) -> let vernac_gen_expr = ast.v.expr in let type_, statement = match vernac_gen_expr with @@ -169,7 +195,7 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out | None -> outline | Some type_ -> let range = range_of_id document id in - let element = {id; type_; name; statement; range} in + let element = {id; type_; name; statement; range; proof=[]} in element :: outline end | VtSideff (names, _) -> @@ -191,7 +217,7 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out | None -> outline | Some type_ -> let range = range_of_id document id in - let element = {id; type_; name; statement; range} in + let element = {id; type_; name; statement; range; proof=[]} in element :: outline end | _ -> outline diff --git a/language-server/dm/document.mli b/language-server/dm/document.mli index 03cbc305..43cf83f8 100644 --- a/language-server/dm/document.mli +++ b/language-server/dm/document.mli @@ -27,12 +27,19 @@ type proof_block_type = | DefinitionType of Decls.definition_object_kind | Other +type proof_step = { + id: sentence_id; + tactic: string; + range: Range.t; +} + type outline_element = { id: sentence_id; name: string; type_: proof_block_type; statement: string; - range: Range.t + proof: proof_step list; + range: Range.t; } type outline = outline_element list diff --git a/language-server/dm/rawDocument.ml b/language-server/dm/rawDocument.ml index cdb3732f..6bf6bd8a 100644 --- a/language-server/dm/rawDocument.ml +++ b/language-server/dm/rawDocument.ml @@ -102,6 +102,12 @@ let word_at_position raw pos : string option = with _ -> None +let string_in_range raw start end_ = + try + String.sub raw.text start (end_ - start) + with _ -> (* TODO: ERROR *) + "" + let apply_text_edit raw (Range.{start; end_}, editText) = let start = loc_of_position raw start in let stop = loc_of_position raw end_ in diff --git a/language-server/dm/rawDocument.mli b/language-server/dm/rawDocument.mli index 9ab8b74c..5f72d407 100644 --- a/language-server/dm/rawDocument.mli +++ b/language-server/dm/rawDocument.mli @@ -26,6 +26,7 @@ val end_loc : t -> int val range_of_loc : t -> Loc.t -> Range.t val word_at_position: t -> Position.t -> string option +val string_in_range: t -> int -> int -> string (** Applies a text edit, and returns start location *) val apply_text_edit : t -> text_edit -> t * int From 242788dede394e27c92ed0d3f6c114f1db212070 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Fri, 6 Dec 2024 11:44:45 +0100 Subject: [PATCH 02/10] feat: make the statement of a theorem part of the outline --- language-server/dm/document.ml | 15 ++++++++------- 1 file changed, 8 insertions(+), 7 deletions(-) diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index 3c3570ee..a71c81e9 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -179,13 +179,13 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out | VtProofStep _ -> push_proof_step_in_outline document id outline | VtStartProof (_, names) -> let vernac_gen_expr = ast.v.expr in - let type_, statement = match vernac_gen_expr with - | VernacSynterp _ -> None, "" + let type_ = match vernac_gen_expr with + | VernacSynterp _ -> None | VernacSynPure pure -> match pure with - | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind), "theorem" - | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def), "definition" - | _ -> None, "" + | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind) + | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def) + | _ -> None in let name = match names with |[] -> "default" @@ -195,6 +195,7 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out | None -> outline | Some type_ -> let range = range_of_id document id in + let statement = string_of_id document id in let element = {id; type_; name; statement; range; proof=[]} in element :: outline end @@ -205,8 +206,8 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out | VernacSynterp _ -> None, "" | VernacSynPure pure -> match pure with - | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind), "theroem" - | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def), "definition" + | Vernacexpr.VernacStartTheoremProof (kind, _) -> Some (TheoremKind kind), string_of_id document id + | Vernacexpr.VernacDefinition ((_, def), _, _) -> Some (DefinitionType def), string_of_id document id | _ -> None, "" in let name = match names with From d2e9efc612cf4b59b675a4fb5e8fdce0c021db00 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Fri, 6 Dec 2024 11:45:17 +0100 Subject: [PATCH 03/10] feat: add language server lsp API to get document proofs --- language-server/dm/documentManager.ml | 18 ++++++++++++++++++ language-server/dm/documentManager.mli | 2 ++ language-server/protocol/extProtocol.ml | 21 +++++++++++++++++++++ language-server/protocol/proofState.ml | 18 +++++++++++++++++- language-server/protocol/proofState.mli | 9 ++++++++- language-server/vscoqtop/lspManager.ml | 9 +++++++++ 6 files changed, 75 insertions(+), 2 deletions(-) diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index bf777dbc..ab0d6af0 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -319,6 +319,24 @@ let observe ~background state id ~should_block_on_error : (state * event Sel.Eve let reset_to_top st = { st with observe_id = Top } + +let get_document_proofs st = + let outline = Document.outline st.document in + let is_theorem Document.{ type_ } = + match type_ with + | TheoremKind _ -> true + | _ -> false + in + let mk_proof_block Document.{statement; proof; range } = + let steps = List.map (fun Document.{tactic; range} -> ProofState.mk_proof_step tactic range) proof in + let step_ranges = List.map (fun (x: Document.proof_step) -> x.range) proof in + let range = List.fold_right RangeList.insert_or_merge_range step_ranges [range] in + let range = List.hd range in + ProofState.mk_proof_block statement steps range + in + let proofs, _ = List.partition is_theorem outline in + List.map mk_proof_block proofs + let get_document_symbols st = let outline = Document.outline st.document in let to_document_symbol elem = diff --git a/language-server/dm/documentManager.mli b/language-server/dm/documentManager.mli index c5780b54..dff6d16e 100644 --- a/language-server/dm/documentManager.mli +++ b/language-server/dm/documentManager.mli @@ -110,6 +110,8 @@ val get_info_messages : state -> Position.t option -> (DiagnosticSeverity.t * pp val get_document_symbols : state -> DocumentSymbol.t list +val get_document_proofs : state -> ProofState.proof_block list + val all_diagnostics : state -> Diagnostic.t list (** all_diagnostics [doc] returns the diagnostics corresponding to the sentences that have been executed in [doc]. *) diff --git a/language-server/protocol/extProtocol.ml b/language-server/protocol/extProtocol.ml index 248ef971..0175f36d 100644 --- a/language-server/protocol/extProtocol.ml +++ b/language-server/protocol/extProtocol.ml @@ -248,6 +248,22 @@ module Request = struct end + module DocumentProofsParams = struct + + type t = { + textDocument: VersionedTextDocumentIdentifier.t + } [@@deriving yojson] + + end + + module DocumentProofsResult = struct + + type t = { + proofs: ProofState.proof_block list; + } [@@deriving yojson] + + end + type 'a t = | Std : 'a Lsp.Client_request.t -> 'a t | Reset : ResetParams.t -> unit t @@ -257,6 +273,7 @@ module Request = struct | Print : PrintParams.t -> pp t | Search : SearchParams.t -> unit t | DocumentState : DocumentStateParams.t -> DocumentStateResult.t t + | DocumentProofs : DocumentProofsParams.t -> DocumentProofsResult.t t type packed = Pack : 'a t -> packed @@ -284,6 +301,9 @@ module Request = struct | "vscoq/documentState" -> let+ params = Lsp.Import.Json.message_params params DocumentStateParams.t_of_yojson in Pack (DocumentState params) + | "vscoq/documentProofs" -> + let+ params = Lsp.Import.Json.message_params params DocumentProofsParams.t_of_yojson in + Pack (DocumentProofs params) | _ -> let+ E req = Lsp.Client_request.of_jsonrpc req in Pack (Std req) @@ -298,6 +318,7 @@ module Request = struct | Print _ -> yojson_of_pp resp | Search _ -> yojson_of_unit resp | DocumentState _ -> DocumentStateResult.(yojson_of_t resp) + | DocumentProofs _ -> DocumentProofsResult.(yojson_of_t resp) | Std req -> Lsp.Client_request.yojson_of_result req resp end diff --git a/language-server/protocol/proofState.ml b/language-server/protocol/proofState.ml index 31204008..004e3222 100644 --- a/language-server/protocol/proofState.ml +++ b/language-server/protocol/proofState.ml @@ -13,9 +13,21 @@ (**************************************************************************) open Printing +open Lsp.Types open Ppx_yojson_conv_lib.Yojson_conv.Primitives +type proof_step = { + tactic: string; + range: Range.t; +} [@@deriving yojson] + +type proof_block = { + statement: string; + range: Range.t; + steps: proof_step list; +} [@@deriving yojson] + type goal = { id: int; hypotheses: pp list; @@ -118,4 +130,8 @@ let get_proof ~previous diff_mode st = shelvedGoals; givenUpGoals; unfocusedGoals; - } \ No newline at end of file + } + +let mk_proof_step tactic range = {tactic; range} + +let mk_proof_block statement steps range = {statement; steps; range} \ No newline at end of file diff --git a/language-server/protocol/proofState.mli b/language-server/protocol/proofState.mli index 5658de21..e1619027 100644 --- a/language-server/protocol/proofState.mli +++ b/language-server/protocol/proofState.mli @@ -13,6 +13,13 @@ (**************************************************************************) open Settings +type proof_step [@@deriving yojson] + +type proof_block [@@deriving yojson] + type t [@@deriving yojson] -val get_proof : previous:Vernacstate.t option -> Goals.Diff.Mode.t -> Vernacstate.t -> t option \ No newline at end of file +val get_proof : previous:Vernacstate.t option -> Goals.Diff.Mode.t -> Vernacstate.t -> t option + +val mk_proof_step : string -> Lsp.Types.Range.t -> proof_step +val mk_proof_block : string -> proof_step list -> Lsp.Types.Range.t -> proof_block \ No newline at end of file diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index a9047774..792ceda1 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -546,6 +546,14 @@ let sendDocumentState id params = | Some { st } -> let document = Dm.DocumentManager.Internal.string_of_state st in Ok Request.Client.DocumentStateResult.{ document }, [] +let sendDocumentProofs id params = + let Request.Client.DocumentProofsParams.{ textDocument } = params in + let uri = textDocument.uri in + match Hashtbl.find_opt states (DocumentUri.to_path uri) with + | None -> log @@ "[documentProofs] ignoring event on non existent document"; Error({message="Document does not exist"; code=None}), [] + | Some { st } -> let proofs = Dm.DocumentManager.get_document_proofs st in + Ok Request.Client.DocumentProofsResult.{ proofs }, [] + let workspaceDidChangeConfiguration params = let Lsp.Types.DidChangeConfigurationParams.{ settings } = params in let settings = Settings.t_of_yojson settings in @@ -582,6 +590,7 @@ let dispatch_request : type a. Jsonrpc.Id.t -> a Request.Client.t -> (a,error) r | Print params -> coqtopPrint id params | Search params -> coqtopSearch id params | DocumentState params -> sendDocumentState id params + | DocumentProofs params -> sendDocumentProofs id params let dispatch_std_notification = let open Lsp.Client_notification in function From 0b05cfbd84d790d7c39c10daaadedd5dace0e66a Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Mon, 9 Dec 2024 11:26:45 +0100 Subject: [PATCH 04/10] feat: add a get document proofs external api Now extensions that depend on vscoq can get all the document proofs. --- client/src/client.ts | 1 - client/src/extension.ts | 26 +++++++++++++++++++++++++- client/src/protocol/types.ts | 19 +++++++++++++++++++ 3 files changed, 44 insertions(+), 2 deletions(-) diff --git a/client/src/client.ts b/client/src/client.ts index b2a88826..091be35c 100644 --- a/client/src/client.ts +++ b/client/src/client.ts @@ -4,7 +4,6 @@ import { LanguageClient, LanguageClientOptions, ServerOptions, - integer } from 'vscode-languageclient/node'; import {decorationsManual, decorationsContinuous, decorationsErrorAnimation} from './Decorations'; diff --git a/client/src/extension.ts b/client/src/extension.ts index 138ba9a7..8d4e64c6 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -27,6 +27,8 @@ import GoalPanel from './panels/GoalPanel'; import SearchViewProvider from './panels/SearchViewProvider'; import { CoqLogMessage, + DocumentProofsRequest, + DocumentProofsResponse, ErrorAlertNotification, MoveCursorNotification, ProofViewNotification, @@ -186,6 +188,22 @@ export function activate(context: ExtensionContext) { }); }; + const getDocumentProofs = (editor: TextEditor) => { + const uri = editor.document.uri; + const textDocument = TextDocumentIdentifier.create(uri.toString()); + const params: DocumentProofsRequest = {textDocument}; + const req = new RequestType("vscoq/documentProofs"); + Client.writeToVscoq2Channel("Getting proofs for: " + uri.toString()); + client.sendRequest(req, params).then( + (res) => { + return res; + }, + (err) => { + window.showErrorMessage(err); + } + ); + }; + registerVscoqTextCommand('reset', (editor) => { const uri = editor.document.uri; const textDocument = TextDocumentIdentifier.create(uri.toString()); @@ -368,7 +386,13 @@ Path: \`${coqTM.getVsCoqTopPath()}\` }); context.subscriptions.push(client); - } + + const externalApi = { + getDocumentProofs + }; + + return externalApi; + } } diff --git a/client/src/protocol/types.ts b/client/src/protocol/types.ts index b8ae64c1..74b555f5 100644 --- a/client/src/protocol/types.ts +++ b/client/src/protocol/types.ts @@ -144,3 +144,22 @@ export interface ResetCoqRequest { } export interface ResetCoqResponse {}; + +export interface DocumentProofsRequest { + textDocument: TextDocumentIdentifier; +} + +type proof_step = { + range: Range; + tactic: string; +}; + +type proof_block = { + statement: string; + range: Range; + proofs: proof_step[]; +}; + +export interface DocumentProofsResponse { + proofs: proof_block[]; +} From bcedd85880e1ee66ff0e69e074585eb9af3c469e Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Mon, 9 Dec 2024 12:08:07 +0100 Subject: [PATCH 05/10] fix: only pass the URI to the API function --- client/src/extension.ts | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/client/src/extension.ts b/client/src/extension.ts index 8d4e64c6..a1f240a2 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -17,6 +17,7 @@ import { RequestType, ServerOptions, TextDocumentIdentifier, + VersionedTextDocumentIdentifier, } from 'vscode-languageclient/node'; import Client from './client'; @@ -188,8 +189,7 @@ export function activate(context: ExtensionContext) { }); }; - const getDocumentProofs = (editor: TextEditor) => { - const uri = editor.document.uri; + const getDocumentProofs = (uri: VersionedTextDocumentIdentifier) => { const textDocument = TextDocumentIdentifier.create(uri.toString()); const params: DocumentProofsRequest = {textDocument}; const req = new RequestType("vscoq/documentProofs"); From 5727911bac1b45a3d7c11253538bdfb8113fc2c5 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Mon, 9 Dec 2024 13:53:38 +0100 Subject: [PATCH 06/10] fix: send the api from activate function --- client/src/extension.ts | 40 ++++++++++++++++++++-------------------- 1 file changed, 20 insertions(+), 20 deletions(-) diff --git a/client/src/extension.ts b/client/src/extension.ts index a1f240a2..f80dcea6 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -62,6 +62,21 @@ export function activate(context: ExtensionContext) { }); } + const getDocumentProofs = (uri: VersionedTextDocumentIdentifier) => { + const textDocument = TextDocumentIdentifier.create(uri.toString()); + const params: DocumentProofsRequest = {textDocument}; + const req = new RequestType("vscoq/documentProofs"); + Client.writeToVscoq2Channel("Getting proofs for: " + uri.toString()); + client.sendRequest(req, params).then( + (res) => { + return res; + }, + (err) => { + window.showErrorMessage(err); + } + ); + }; + // Watch for files being added or removed workspace.onDidCreateFiles(checkInCoqProject); workspace.onDidDeleteFiles(checkInCoqProject); @@ -189,21 +204,6 @@ export function activate(context: ExtensionContext) { }); }; - const getDocumentProofs = (uri: VersionedTextDocumentIdentifier) => { - const textDocument = TextDocumentIdentifier.create(uri.toString()); - const params: DocumentProofsRequest = {textDocument}; - const req = new RequestType("vscoq/documentProofs"); - Client.writeToVscoq2Channel("Getting proofs for: " + uri.toString()); - client.sendRequest(req, params).then( - (res) => { - return res; - }, - (err) => { - window.showErrorMessage(err); - } - ); - }; - registerVscoqTextCommand('reset', (editor) => { const uri = editor.document.uri; const textDocument = TextDocumentIdentifier.create(uri.toString()); @@ -386,13 +386,13 @@ Path: \`${coqTM.getVsCoqTopPath()}\` }); context.subscriptions.push(client); + } - const externalApi = { - getDocumentProofs - }; + const externalApi = { + getDocumentProofs + }; - return externalApi; - } + return externalApi; } From 16ae8d088ed9847d41985ca40fd8a2d001d01bd7 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Tue, 10 Dec 2024 11:19:04 +0100 Subject: [PATCH 07/10] fix: simplify api + return promise --- client/src/extension.ts | 12 ++---------- language-server/protocol/extProtocol.ml | 2 +- 2 files changed, 3 insertions(+), 11 deletions(-) diff --git a/client/src/extension.ts b/client/src/extension.ts index f80dcea6..f60a0149 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -17,7 +17,6 @@ import { RequestType, ServerOptions, TextDocumentIdentifier, - VersionedTextDocumentIdentifier, } from 'vscode-languageclient/node'; import Client from './client'; @@ -62,19 +61,12 @@ export function activate(context: ExtensionContext) { }); } - const getDocumentProofs = (uri: VersionedTextDocumentIdentifier) => { + const getDocumentProofs = (uri: Uri) => { const textDocument = TextDocumentIdentifier.create(uri.toString()); const params: DocumentProofsRequest = {textDocument}; const req = new RequestType("vscoq/documentProofs"); Client.writeToVscoq2Channel("Getting proofs for: " + uri.toString()); - client.sendRequest(req, params).then( - (res) => { - return res; - }, - (err) => { - window.showErrorMessage(err); - } - ); + return client.sendRequest(req, params); }; // Watch for files being added or removed diff --git a/language-server/protocol/extProtocol.ml b/language-server/protocol/extProtocol.ml index 0175f36d..ca863b13 100644 --- a/language-server/protocol/extProtocol.ml +++ b/language-server/protocol/extProtocol.ml @@ -251,7 +251,7 @@ module Request = struct module DocumentProofsParams = struct type t = { - textDocument: VersionedTextDocumentIdentifier.t + textDocument: TextDocumentIdentifier.t } [@@deriving yojson] end From a3b30ba004695f335dc6e1610ccef8cf2de903c0 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Tue, 10 Dec 2024 13:35:51 +0100 Subject: [PATCH 08/10] fix: give a more accurate representation of proof block --- client/src/protocol/types.ts | 15 ++++++++++----- language-server/dm/document.ml | 2 +- language-server/dm/documentManager.ml | 8 +++++--- language-server/protocol/proofState.ml | 11 +++++++++-- language-server/protocol/proofState.mli | 5 ++++- 5 files changed, 29 insertions(+), 12 deletions(-) diff --git a/client/src/protocol/types.ts b/client/src/protocol/types.ts index 74b555f5..c72a3e8a 100644 --- a/client/src/protocol/types.ts +++ b/client/src/protocol/types.ts @@ -149,17 +149,22 @@ export interface DocumentProofsRequest { textDocument: TextDocumentIdentifier; } -type proof_step = { +type ProofStatement = { + range: Range; + statement: string; +} + +type ProofStep = { range: Range; tactic: string; }; -type proof_block = { - statement: string; +type ProofBlock = { + statement: ProofStatement; range: Range; - proofs: proof_step[]; + steps: ProofStep[]; }; export interface DocumentProofsResponse { - proofs: proof_block[]; + proofs: ProofBlock[]; } diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index a71c81e9..a32cae5b 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -176,7 +176,7 @@ let push_proof_step_in_outline document id (outline : outline) = let record_outline document id (ast : Synterp.vernac_control_entry) classif (outline : outline) = let open Vernacextend in match classif with - | VtProofStep _ -> push_proof_step_in_outline document id outline + | VtProofStep _ | VtQed _ -> push_proof_step_in_outline document id outline | VtStartProof (_, names) -> let vernac_gen_expr = ast.v.expr in let type_ = match vernac_gen_expr with diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index ab0d6af0..58d2377f 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -328,10 +328,12 @@ let get_document_proofs st = | _ -> false in let mk_proof_block Document.{statement; proof; range } = + let statement = ProofState.mk_proof_statement statement range in + let last_step = List.hd proof in + let proof = List.rev proof in + let fst_step = List.hd proof in + let range = Range.create ~start:fst_step.range.start ~end_:last_step.range.end_ in let steps = List.map (fun Document.{tactic; range} -> ProofState.mk_proof_step tactic range) proof in - let step_ranges = List.map (fun (x: Document.proof_step) -> x.range) proof in - let range = List.fold_right RangeList.insert_or_merge_range step_ranges [range] in - let range = List.hd range in ProofState.mk_proof_block statement steps range in let proofs, _ = List.partition is_theorem outline in diff --git a/language-server/protocol/proofState.ml b/language-server/protocol/proofState.ml index 004e3222..86549cbb 100644 --- a/language-server/protocol/proofState.ml +++ b/language-server/protocol/proofState.ml @@ -17,13 +17,18 @@ open Lsp.Types open Ppx_yojson_conv_lib.Yojson_conv.Primitives +type proof_statement = { + statement: string; + range: Range.t; +} [@@deriving yojson] + type proof_step = { tactic: string; range: Range.t; } [@@deriving yojson] type proof_block = { - statement: string; + statement: proof_statement; range: Range.t; steps: proof_step list; } [@@deriving yojson] @@ -132,6 +137,8 @@ let get_proof ~previous diff_mode st = unfocusedGoals; } +let mk_proof_statement statement range = {statement; range} + let mk_proof_step tactic range = {tactic; range} -let mk_proof_block statement steps range = {statement; steps; range} \ No newline at end of file +let mk_proof_block statement steps range = {steps; statement; range} \ No newline at end of file diff --git a/language-server/protocol/proofState.mli b/language-server/protocol/proofState.mli index e1619027..0acf7f23 100644 --- a/language-server/protocol/proofState.mli +++ b/language-server/protocol/proofState.mli @@ -13,6 +13,8 @@ (**************************************************************************) open Settings +type proof_statement [@@deriving yojson] + type proof_step [@@deriving yojson] type proof_block [@@deriving yojson] @@ -21,5 +23,6 @@ type t [@@deriving yojson] val get_proof : previous:Vernacstate.t option -> Goals.Diff.Mode.t -> Vernacstate.t -> t option +val mk_proof_statement : string -> Lsp.Types.Range.t -> proof_statement val mk_proof_step : string -> Lsp.Types.Range.t -> proof_step -val mk_proof_block : string -> proof_step list -> Lsp.Types.Range.t -> proof_block \ No newline at end of file +val mk_proof_block : proof_statement -> proof_step list -> Lsp.Types.Range.t -> proof_block \ No newline at end of file From 8ba72e935bfca2a722fa998f7ff79b0eba53a063 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Tue, 10 Dec 2024 15:15:52 +0100 Subject: [PATCH 09/10] fix: recompute the outline entirely once a document as re-parsed Before we would only add new sentences during the parsing phase, which works on the first parsing but leads to unwanted behaviors after an edit. --- language-server/dm/document.ml | 10 +++++++--- 1 file changed, 7 insertions(+), 3 deletions(-) diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index a32cae5b..b19bd1d8 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -223,6 +223,10 @@ let record_outline document id (ast : Synterp.vernac_control_entry) classif (out end | _ -> outline +let compute_outline ({ sentences_by_end } as document) = + LM.fold (fun _ {id; ast} -> record_outline document id ast.ast ast.classification) sentences_by_end [] + + let schedule doc = doc.schedule let raw_document doc = doc.raw_doc @@ -244,8 +248,7 @@ let add_sentence parsed parsing_start start stop (ast: parsed_ast) synterp_state sentences_by_id = SM.add id sentence parsed.sentences_by_id; schedule; } in - let outline = record_outline document id ast.ast ast.classification parsed.outline in - {document with outline}, scheduler_state_after + document, scheduler_state_after let remove_sentence parsed id = match SM.find_opt id parsed.sentences_by_id with @@ -649,7 +652,8 @@ let handle_invalidate {parsed; errors; parsed_comments; stop; top_id; started; p List.fold_left (fun acc (comment : comment) -> LM.add comment.stop comment acc) comments new_comments in let parsed_loc = pos_at_end document in - let parsed_document = {document with parsed_loc; parsing_errors_by_end; comments_by_end} in + let outline = compute_outline document in + let parsed_document = {document with parsed_loc; parsing_errors_by_end; comments_by_end; outline} in Some {parsed_document; unchanged_id; invalid_ids; previous_document} let handle_event document = function From 18472f0653f7a022e84548f5b4b6cd4a37d17920 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Tue, 10 Dec 2024 15:28:02 +0100 Subject: [PATCH 10/10] feat: add error if document is parsing If the document is parsing, the document should resend the documentProofs request later. --- language-server/vscoqtop/lspManager.ml | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/language-server/vscoqtop/lspManager.ml b/language-server/vscoqtop/lspManager.ml index 792ceda1..f09cf415 100644 --- a/language-server/vscoqtop/lspManager.ml +++ b/language-server/vscoqtop/lspManager.ml @@ -551,8 +551,12 @@ let sendDocumentProofs id params = let uri = textDocument.uri in match Hashtbl.find_opt states (DocumentUri.to_path uri) with | None -> log @@ "[documentProofs] ignoring event on non existent document"; Error({message="Document does not exist"; code=None}), [] - | Some { st } -> let proofs = Dm.DocumentManager.get_document_proofs st in - Ok Request.Client.DocumentProofsResult.{ proofs }, [] + | Some { st } -> + if Dm.DocumentManager.is_parsing st then + Error {code=(Some Jsonrpc.Response.Error.Code.ServerCancelled); message="Parsing not finished"} , [] + else + let proofs = Dm.DocumentManager.get_document_proofs st in + Ok Request.Client.DocumentProofsResult.{ proofs }, [] let workspaceDidChangeConfiguration params = let Lsp.Types.DidChangeConfigurationParams.{ settings } = params in