From d0146c4a008565d84041e38adf3546d89b55e6b0 Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 17 Jan 2024 11:19:13 +0100 Subject: [PATCH 1/8] Quick fix proof of concept. --- client/src/extension.ts | 18 +++++-- client/yarn.lock | 10 ++++ language-server/dm/documentManager.ml | 71 +++++++++++++++++++++++--- language-server/protocol/lspWrapper.ml | 41 +++++++++++++-- 4 files changed, 128 insertions(+), 12 deletions(-) diff --git a/client/src/extension.ts b/client/src/extension.ts index c1cf587b..485e79bc 100644 --- a/client/src/extension.ts +++ b/client/src/extension.ts @@ -1,4 +1,4 @@ -import {workspace, window, commands, ExtensionContext, +import {workspace, window, commands, languages, ExtensionContext, TextEditorSelectionChangeEvent, TextEditorSelectionChangeKind, TextEditor, @@ -9,7 +9,9 @@ import {workspace, window, commands, ExtensionContext, StatusBarItem, extensions, StatusBarAlignment, - MarkdownString + MarkdownString, + TextEdit, + WorkspaceEdit } from 'vscode'; import { @@ -44,7 +46,7 @@ import { } from './utilities/utils'; import { DocumentStateViewProvider } from './panels/DocumentStateViewProvider'; import VsCoqToolchainManager, {ToolchainError, ToolChainErrorCode} from './utilities/toolchain'; -import { stat } from 'fs'; +import { QUICKFIX_COMMAND, CoqWarningQuickFix } from './QuickFixProvider'; let client: Client; @@ -247,6 +249,16 @@ export function activate(context: ExtensionContext) { GoalPanel.proofViewNotification(context.extensionUri, editor, proofView); }); + context.subscriptions.push(commands.registerCommand(QUICKFIX_COMMAND, (data) => { + const {text, range, document} = data; + const edit = new WorkspaceEdit(); + edit.replace(document.uri, range, text); + workspace.applyEdit(edit); + })); + languages.registerCodeActionsProvider('coq', new CoqWarningQuickFix(), { + providedCodeActionKinds: CoqWarningQuickFix.providedCodeActionKinds + }); + client.start() .then(() => { diff --git a/client/yarn.lock b/client/yarn.lock index 0d0e935f..81f10eb3 100644 --- a/client/yarn.lock +++ b/client/yarn.lock @@ -1759,6 +1759,16 @@ jszip@^3.10.1: readable-stream "~2.3.6" setimmediate "^1.0.5" +jszip@^3.10.1: + version "3.10.1" + resolved "https://registry.yarnpkg.com/jszip/-/jszip-3.10.1.tgz#34aee70eb18ea1faec2f589208a157d1feb091c2" + integrity sha512-xXDvecyTpGLrqFrvkrUSoxxfJI5AH7U8zxxtVclpsUtMCq4JQ290LY8AW5c7Ggnr/Y/oK+bQMbqK2qmtk3pN4g== + dependencies: + lie "~3.3.0" + pako "~1.0.2" + readable-stream "~2.3.6" + setimmediate "^1.0.5" + keytar@^7.7.0: version "7.9.0" resolved "https://registry.yarnpkg.com/keytar/-/keytar-7.9.0.tgz#4c6225708f51b50cbf77c5aae81721964c2918cb" diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index a5697460..235350af 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -114,16 +114,40 @@ let observe_id_range st = let range = Range.{ start; end_ } in Some range -let make_diagnostic doc range oloc message severity = +let make_diagnostic doc range oloc message severity code = let range = match oloc with | None -> range | Some loc -> RawDocument.range_of_loc (Document.raw_document doc) loc in - Diagnostic.create ~range ~message ~severity () + let code, data = + match code with + | None -> None, None + | Some (x,z) -> Some x, Some z in + Diagnostic.create ?code ?data ~range ~message ~severity () let mk_diag st (id,(lvl,oloc,msg)) = + let code = + match lvl with + | Feedback.Warning quickfixes when oloc <> None -> + let code : Jsonrpc.Id.t * Lsp.Import.Json.t = + let open Lsp.Import.Json in + (`String "quickfix-replace", + quickfixes |> yojson_of_list + (fun pp -> + let s = Pp.string_of_ppcmds pp in + let range = + match oloc with + | None -> assert false + | Some loc -> + RawDocument.range_of_loc (Document.raw_document st.document) loc + in + QuickFixData.yojson_of_t (QuickFixData.{range; text = s}) + )) + in + Some code + | _ -> None in let lvl = DiagnosticSeverity.of_feedback_level lvl in make_diagnostic st.document (Document.range_of_id st.document id) oloc (Pp.string_of_ppcmds msg) lvl @@ -144,10 +168,45 @@ let all_diagnostics st = (* we are resilient to a state where invalidate was not called yet *) let exists (id,_) = Option.has_some (Document.get_sentence st.document id) in let exec_errors = all_exec_errors |> List.filter exists in - let feedback = all_feedback |> List.filter exists in - List.map (mk_parsing_error_diag st) parse_errors @ - List.map (mk_error_diag st) exec_errors @ - List.map (mk_diag st) feedback + let warnings_and_errors (id, (lvl, oloc, msg)) = + match lvl with + | Feedback.Warning quickfixes when oloc <> None -> + let code : Jsonrpc.Id.t * Lsp.Import.Json.t = + let open Lsp.Import.Json in + (`String "quickfix-replace", + quickfixes |> yojson_of_list + (fun pp -> + let s = Pp.string_of_ppcmds pp in + let range = + match oloc with + | None -> assert false + | Some loc -> + RawDocument.range_of_loc (Document.raw_document st.document) loc + in + yojson_of_list (fun x -> x) [Range.yojson_of_t range;of_string s]) + ) + in + Some (id, (DiagnosticSeverity.Warning, oloc, msg, Some code)) + | Feedback.Warning _ -> Some (id, (DiagnosticSeverity.Warning, oloc, msg, None)) + | Feedback.Error -> Some (id, (DiagnosticSeverity.Error, oloc, msg, None)) + | _ -> None + in + let diags = all_feedback |> List.filter exists |> List.filter_map warnings_and_errors in + let mk_diag (id,(lvl,oloc,msg,code)) = + make_diagnostic st.document (Document.range_of_id st.document id) oloc msg lvl code + in + let mk_error_diag (id,(oloc,msg)) = mk_diag (id,(DiagnosticSeverity.Error,oloc,msg,None)) in + let mk_parsing_error_diag Document.{ msg = (oloc,msg); start; stop } = + let doc = Document.raw_document st.document in + let severity = DiagnosticSeverity.Error in + let start = RawDocument.position_of_loc doc start in + let end_ = RawDocument.position_of_loc doc stop in + let range = Range.{ start; end_ } in + make_diagnostic st.document range oloc msg severity None + in + List.map mk_parsing_error_diag parse_errors @ + List.map mk_error_diag exec_errors @ + List.map mk_diag diags let id_of_pos st pos = let loc = RawDocument.loc_of_position (Document.raw_document st.document) pos in diff --git a/language-server/protocol/lspWrapper.ml b/language-server/protocol/lspWrapper.ml index e1f5d8c0..17864cac 100644 --- a/language-server/protocol/lspWrapper.ml +++ b/language-server/protocol/lspWrapper.ml @@ -3,7 +3,7 @@ (* VSCoq *) (* *) (* Copyright INRIA and contributors *) -(* (see version control and README file for authors & dates) *) +(* (see version control and README file for authors & dates)Variables A : Type. *) (* *) (**************************************************************************) (* *) @@ -66,6 +66,10 @@ module Range = struct end +module QuickFixData = struct + type t = {text: string; range: Range.t} [@@deriving yojson] +end + module DiagnosticSeverity = struct type t = [%import: Lsp.Types.DiagnosticSeverity.t] [@@deriving sexp] @@ -74,12 +78,43 @@ module DiagnosticSeverity = struct let t_of_yojson v = Lsp.Types.DiagnosticSeverity.t_of_yojson v let of_feedback_level = let open DiagnosticSeverity in function - | Feedback.Error -> Error - | Feedback.Warning -> Warning + | Feedback.Error -> Some Error + | Feedback.Warning _ -> Some Warning | Feedback.(Info | Debug | Notice) -> Information end +module FeedbackChannel = struct + + type t = + | Debug + | Info + | Notice + [@@deriving sexp, yojson] + + let yojson_of_t = function + | Debug -> `Int 0 + | Info -> `Int 1 + | Notice -> `Int 2 + + let t_of_feedback_level = function + | Feedback.Debug -> Some Debug + | Feedback.Info -> Some Info + | Feedback.Notice -> Some Notice + | Feedback.(Error | Warning _) -> Information + +end + +module CoqFeedback = struct + + type t = { + range: Range.t; + message: string; + channel: FeedbackChannel.t; + } [@@deriving sexp, yojson] + +end + type query_result = { id : string; name : pp; From 1521266335cd5092fdd6a99bcaac20daacc03b3e Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Wed, 5 Jun 2024 14:13:47 +0200 Subject: [PATCH 2/8] Finish rebasing --- flake.lock | 2 +- language-server/dm/document.ml | 4 +- language-server/dm/documentManager.ml | 51 ++++---------------------- language-server/protocol/lspWrapper.ml | 6 +-- 4 files changed, 14 insertions(+), 49 deletions(-) diff --git a/flake.lock b/flake.lock index e94a7faa..107343a4 100644 --- a/flake.lock +++ b/flake.lock @@ -16,7 +16,7 @@ "type": "github" }, "original": { - "owner": "coq", + "owner": "gares", "repo": "coq", "rev": "e139cf972cf2a876583ebbf5a19ffd419828116b", "type": "github" diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index 9811cfec..8e9e120a 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -336,8 +336,8 @@ let get_loc_from_info_or_exn exn = let get_entry ast = Synterp.synterp_control ast [%%else] let get_entry ast = - let intern = Vernacinterp.fs_intern in - Synterp.synterp_control ~intern ast + (* let intern = Vernacinterp.fs_intern in *) + Synterp.synterp_control ast [%%endif] let rec parse_more synterp_state stream raw parsed parsed_comments errors = diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 235350af..ebf7725c 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -149,7 +149,7 @@ let mk_diag st (id,(lvl,oloc,msg)) = Some code | _ -> None in let lvl = DiagnosticSeverity.of_feedback_level lvl in - make_diagnostic st.document (Document.range_of_id st.document id) oloc (Pp.string_of_ppcmds msg) lvl + make_diagnostic st.document (Document.range_of_id st.document id) oloc (Pp.string_of_ppcmds msg) lvl code let mk_error_diag st (id,(oloc,msg)) = mk_diag st (id,(Feedback.Error,oloc, msg)) @@ -159,7 +159,7 @@ let mk_parsing_error_diag st Document.{ msg = (oloc,msg); start; stop } = let start = RawDocument.position_of_loc doc start in let end_ = RawDocument.position_of_loc doc stop in let range = Range.{ start; end_ } in - make_diagnostic st.document range oloc msg severity + make_diagnostic st.document range oloc msg severity None let all_diagnostics st = let parse_errors = Document.parse_errors st.document in @@ -168,45 +168,10 @@ let all_diagnostics st = (* we are resilient to a state where invalidate was not called yet *) let exists (id,_) = Option.has_some (Document.get_sentence st.document id) in let exec_errors = all_exec_errors |> List.filter exists in - let warnings_and_errors (id, (lvl, oloc, msg)) = - match lvl with - | Feedback.Warning quickfixes when oloc <> None -> - let code : Jsonrpc.Id.t * Lsp.Import.Json.t = - let open Lsp.Import.Json in - (`String "quickfix-replace", - quickfixes |> yojson_of_list - (fun pp -> - let s = Pp.string_of_ppcmds pp in - let range = - match oloc with - | None -> assert false - | Some loc -> - RawDocument.range_of_loc (Document.raw_document st.document) loc - in - yojson_of_list (fun x -> x) [Range.yojson_of_t range;of_string s]) - ) - in - Some (id, (DiagnosticSeverity.Warning, oloc, msg, Some code)) - | Feedback.Warning _ -> Some (id, (DiagnosticSeverity.Warning, oloc, msg, None)) - | Feedback.Error -> Some (id, (DiagnosticSeverity.Error, oloc, msg, None)) - | _ -> None - in - let diags = all_feedback |> List.filter exists |> List.filter_map warnings_and_errors in - let mk_diag (id,(lvl,oloc,msg,code)) = - make_diagnostic st.document (Document.range_of_id st.document id) oloc msg lvl code - in - let mk_error_diag (id,(oloc,msg)) = mk_diag (id,(DiagnosticSeverity.Error,oloc,msg,None)) in - let mk_parsing_error_diag Document.{ msg = (oloc,msg); start; stop } = - let doc = Document.raw_document st.document in - let severity = DiagnosticSeverity.Error in - let start = RawDocument.position_of_loc doc start in - let end_ = RawDocument.position_of_loc doc stop in - let range = Range.{ start; end_ } in - make_diagnostic st.document range oloc msg severity None - in - List.map mk_parsing_error_diag parse_errors @ - List.map mk_error_diag exec_errors @ - List.map mk_diag diags + let feedback = all_feedback |> List.filter exists in + List.map (mk_parsing_error_diag st) parse_errors @ + 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 @@ -342,8 +307,8 @@ let validate_document state = let start_library top opts = Coqinit.start_library ~top opts [%%else] let start_library top opts = - let intern = Vernacinterp.fs_intern in - Coqinit.start_library ~intern ~top opts; + (* let intern = Vernacinterp.fs_intern in *) + Coqinit.start_library ~top opts; [%%endif] let init init_vs ~opts uri ~text observe_id = diff --git a/language-server/protocol/lspWrapper.ml b/language-server/protocol/lspWrapper.ml index 17864cac..c15af6c3 100644 --- a/language-server/protocol/lspWrapper.ml +++ b/language-server/protocol/lspWrapper.ml @@ -78,8 +78,8 @@ module DiagnosticSeverity = struct let t_of_yojson v = Lsp.Types.DiagnosticSeverity.t_of_yojson v let of_feedback_level = let open DiagnosticSeverity in function - | Feedback.Error -> Some Error - | Feedback.Warning _ -> Some Warning + | Feedback.Error -> Error + | Feedback.Warning _ -> Warning | Feedback.(Info | Debug | Notice) -> Information end @@ -101,7 +101,7 @@ module FeedbackChannel = struct | Feedback.Debug -> Some Debug | Feedback.Info -> Some Info | Feedback.Notice -> Some Notice - | Feedback.(Error | Warning _) -> Information + | Feedback.(Error | Warning _) -> None end From 91af99660926f4b85c81620fc978273a1a9c069a Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Wed, 5 Jun 2024 14:51:10 +0200 Subject: [PATCH 3/8] Adapt to new quickfix API --- language-server/dm/document.ml | 4 ++-- language-server/dm/documentManager.ml | 18 +++++++----------- 2 files changed, 9 insertions(+), 13 deletions(-) diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index 8e9e120a..9811cfec 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -336,8 +336,8 @@ let get_loc_from_info_or_exn exn = let get_entry ast = Synterp.synterp_control ast [%%else] let get_entry ast = - (* let intern = Vernacinterp.fs_intern in *) - Synterp.synterp_control ast + let intern = Vernacinterp.fs_intern in + Synterp.synterp_control ~intern ast [%%endif] let rec parse_more synterp_state stream raw parsed parsed_comments errors = diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index ebf7725c..c3cb7c3c 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -130,19 +130,15 @@ let make_diagnostic doc range oloc message severity code = let mk_diag st (id,(lvl,oloc,msg)) = let code = match lvl with - | Feedback.Warning quickfixes when oloc <> None -> + | Feedback.Warning quickfixes -> let code : Jsonrpc.Id.t * Lsp.Import.Json.t = let open Lsp.Import.Json in (`String "quickfix-replace", quickfixes |> yojson_of_list - (fun pp -> - let s = Pp.string_of_ppcmds pp in - let range = - match oloc with - | None -> assert false - | Some loc -> - RawDocument.range_of_loc (Document.raw_document st.document) loc - in + (fun qf -> + let s = Pp.string_of_ppcmds @@ Feedback.Quickfix.pp qf in + let loc = Feedback.Quickfix.loc qf in + let range = RawDocument.range_of_loc (Document.raw_document st.document) loc in QuickFixData.yojson_of_t (QuickFixData.{range; text = s}) )) in @@ -307,8 +303,8 @@ let validate_document state = let start_library top opts = Coqinit.start_library ~top opts [%%else] let start_library top opts = - (* let intern = Vernacinterp.fs_intern in *) - Coqinit.start_library ~top opts; + let intern = Vernacinterp.fs_intern in + Coqinit.start_library ~intern ~top opts; [%%endif] let init init_vs ~opts uri ~text observe_id = From 1ed08ea27d1dacd7c37830550aaeda9dba10f129 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Wed, 5 Jun 2024 16:22:26 +0200 Subject: [PATCH 4/8] Adding the quickfix provider. --- client/src/QuickFixProvider.ts | 46 ++++++++++++++++++++++++++++++++++ 1 file changed, 46 insertions(+) create mode 100644 client/src/QuickFixProvider.ts diff --git a/client/src/QuickFixProvider.ts b/client/src/QuickFixProvider.ts new file mode 100644 index 00000000..e9bcc16e --- /dev/null +++ b/client/src/QuickFixProvider.ts @@ -0,0 +1,46 @@ +import * as vscode from 'vscode'; +import { Command } from 'vscode'; + +const QUICKFIX_REPLACE = 'quickfix-replace'; +export const QUICKFIX_COMMAND = 'vscoq.quickfix'; + +export class QuickFixDiagnostic extends vscode.Diagnostic { + readonly data?: any[]; +} + +/** + * Provides code actions corresponding to diagnostic problems. + */ +export class CoqWarningQuickFix implements vscode.CodeActionProvider { + + public static readonly providedCodeActionKinds = [ + vscode.CodeActionKind.QuickFix + ]; + + provideCodeActions(document: vscode.TextDocument, range: vscode.Range | vscode.Selection, context: vscode.CodeActionContext, token: vscode.CancellationToken): vscode.CodeAction[] { + // for each diagnostic entry that has the matching `code`, create a code action command + return context.diagnostics + .filter(diagnostic => diagnostic.code === QUICKFIX_REPLACE) + .flatMap(diagnostic => this.createCommandCodeAction(diagnostic, document)); + } + + private createCommandCodeAction(diagnostic: QuickFixDiagnostic, document: vscode.TextDocument): vscode.CodeAction[] { + if(diagnostic.data) { + + return diagnostic.data.map(d => { + const action = new vscode.CodeAction(d.text, vscode.CodeActionKind.QuickFix); + const data = { + ...d, + document: document + }; + action.command = { command: QUICKFIX_COMMAND, title: 'Replace', tooltip: 'Replace with the suggested change', arguments: [data] }; + return action; + }); + } + return []; + /* action.command = { command: QUICKFIX_COMMAND, title: 'Replace', tooltip: 'Replace with the suggested change' }; + action.diagnostics = [diagnostic]; + action.isPreferred = true; + return action; */ + } +} \ No newline at end of file From fc331dccd66fa4bad719a31da120aef927e1434c Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Thu, 13 Jun 2024 16:12:35 +0200 Subject: [PATCH 5/8] Fix new API --- language-server/dm/documentManager.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index c3cb7c3c..cbfcda3a 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -136,8 +136,8 @@ let mk_diag st (id,(lvl,oloc,msg)) = (`String "quickfix-replace", quickfixes |> yojson_of_list (fun qf -> - let s = Pp.string_of_ppcmds @@ Feedback.Quickfix.pp qf in - let loc = Feedback.Quickfix.loc qf in + let s = Pp.string_of_ppcmds @@ Quickfix.pp qf in + let loc = Quickfix.loc qf in let range = RawDocument.range_of_loc (Document.raw_document st.document) loc in QuickFixData.yojson_of_t (QuickFixData.{range; text = s}) )) From 9f8799632cb87b4934a71e48174df32024ce3306 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Fri, 14 Jun 2024 13:01:39 +0200 Subject: [PATCH 6/8] [language-server] Add support for quickfixes in errors --- language-server/dm/document.ml | 30 ++++++++++------- language-server/dm/document.mli | 1 + language-server/dm/documentManager.ml | 43 ++++++++++++++++++++++-- language-server/dm/executionManager.ml | 44 +++++++++++++------------ language-server/dm/executionManager.mli | 2 +- 5 files changed, 83 insertions(+), 37 deletions(-) diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index 9811cfec..7d342415 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -62,6 +62,7 @@ type parsing_error = { start: int; stop: int; msg: string Loc.located; + qf: Quickfix.t list option; } type document = { @@ -320,16 +321,16 @@ exception E = Grammar.Error [%%endif] [%%if coq = "8.18" || coq = "8.19"] -let get_loc_from_info_or_exn exn = - let e, info = Exninfo.capture exn in +let get_loc_from_info_or_exn e info = match e with | Synterp.UnmappedLibrary (_, qid) -> qid.loc | Synterp.NotFoundLibrary (_, qid) -> qid.loc | _ -> Loc.get_loc @@ info [%%else] -let get_loc_from_info_or_exn exn = - let _, info = Exninfo.capture exn in - Loc.get_loc @@ info +let get_loc_from_info_or_exn _ info = + Loc.get_loc info + +let get_qf_from_info info = Quickfix.get_qf info [%%endif] [%%if coq = "8.18" || coq = "8.19"] @@ -340,11 +341,12 @@ let get_entry ast = Synterp.synterp_control ~intern ast [%%endif] + let rec parse_more synterp_state stream raw parsed parsed_comments errors = - let handle_parse_error start msg = + let handle_parse_error start msg qf = log @@ "handling parse error at " ^ string_of_int start; let stop = Stream.count stream in - let parsing_error = { msg; start; stop; } in + let parsing_error = { msg; start; stop; qf} in let errors = parsing_error :: errors in parse_more synterp_state stream raw parsed parsed_comments errors in @@ -378,22 +380,26 @@ let rec parse_more synterp_state stream raw parsed parsed_comments errors = parse_more synterp_state stream raw parsed parsed_comments errors with exn -> let e, info = Exninfo.capture exn in - let loc = get_loc_from_info_or_exn exn in - handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) + let loc = get_loc_from_info_or_exn e info in + let qf = get_qf_from_info info in + handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) qf end | exception (E msg as exn) -> let loc = Loc.get_loc @@ Exninfo.info exn in + let qf = Quickfix.get_qf @@ Exninfo.info exn in junk_sentence_end stream; - handle_parse_error start (loc,msg) + handle_parse_error start (loc,msg) qf | exception (CLexer.Error.E e as exn) -> (* May be more problematic to handle for the diff *) let loc = Loc.get_loc @@ Exninfo.info exn in + let qf = Quickfix.get_qf @@ Exninfo.info exn in junk_sentence_end stream; - handle_parse_error start (loc,CLexer.Error.to_string e) + handle_parse_error start (loc,CLexer.Error.to_string e) qf | exception exn -> let e, info = Exninfo.capture exn in let loc = Loc.get_loc @@ info in + let qf = Quickfix.get_qf @@ Exninfo.info exn in junk_sentence_end stream; - handle_parse_error start (loc, "Unexpected parse error: " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) + handle_parse_error start (loc, "Unexpected parse error: " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) qf end let parse_more synterp_state stream raw = diff --git a/language-server/dm/document.mli b/language-server/dm/document.mli index 0b577059..329a5f0a 100644 --- a/language-server/dm/document.mli +++ b/language-server/dm/document.mli @@ -43,6 +43,7 @@ type parsing_error = { start: int; stop: int; msg: string Loc.located; + qf: Quickfix.t list option; } val parse_errors : document -> parsing_error list diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index cbfcda3a..88741044 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -147,15 +147,52 @@ let mk_diag st (id,(lvl,oloc,msg)) = let lvl = DiagnosticSeverity.of_feedback_level lvl in make_diagnostic st.document (Document.range_of_id st.document id) oloc (Pp.string_of_ppcmds msg) lvl code -let mk_error_diag st (id,(oloc,msg)) = mk_diag st (id,(Feedback.Error,oloc, msg)) +let mk_error_diag st (id,(oloc,msg,qf)) = (* mk_diag st (id,(Feedback.Error,oloc, msg)) *) + let code = + match qf with + | None -> None + | Some qf -> + let code : Jsonrpc.Id.t * Lsp.Import.Json.t = + let open Lsp.Import.Json in + (`String "quickfix-replace", + qf |> yojson_of_list + (fun qf -> + let s = Pp.string_of_ppcmds @@ Quickfix.pp qf in + let loc = Quickfix.loc qf in + let range = RawDocument.range_of_loc (Document.raw_document st.document) loc in + QuickFixData.yojson_of_t (QuickFixData.{range; text = s}) + )) + in + Some code + in + let lvl = DiagnosticSeverity.of_feedback_level Feedback.Error in + make_diagnostic st.document (Document.range_of_id st.document id) oloc (Pp.string_of_ppcmds msg) lvl code + -let mk_parsing_error_diag st Document.{ msg = (oloc,msg); start; stop } = +let mk_parsing_error_diag st Document.{ msg = (oloc,msg); start; stop; qf } = let doc = Document.raw_document st.document in let severity = DiagnosticSeverity.Error in let start = RawDocument.position_of_loc doc start in let end_ = RawDocument.position_of_loc doc stop in let range = Range.{ start; end_ } in - make_diagnostic st.document range oloc msg severity None + let code = + match qf with + | None -> None + | Some qf -> + let code : Jsonrpc.Id.t * Lsp.Import.Json.t = + let open Lsp.Import.Json in + (`String "quickfix-replace", + qf |> yojson_of_list + (fun qf -> + let s = Pp.string_of_ppcmds @@ Quickfix.pp qf in + let loc = Quickfix.loc qf in + let range = RawDocument.range_of_loc (Document.raw_document st.document) loc in + QuickFixData.yojson_of_t (QuickFixData.{range; text = s}) + )) + in + Some code + in + make_diagnostic st.document range oloc msg severity code let all_diagnostics st = let parse_errors = Document.parse_errors st.document in diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml index 6df25298..6f63e3bb 100644 --- a/language-server/dm/executionManager.ml +++ b/language-server/dm/executionManager.ml @@ -21,10 +21,10 @@ let Log log = Log.mk_log "executionManager" type execution_status = | Success of Vernacstate.t option - | Error of Pp.t Loc.located * Vernacstate.t option (* State to use for resiliency *) + | Error of Pp.t Loc.located * Quickfix.t list option * Vernacstate.t option (* State to use for resiliency *) let success vernac_st = Success (Some vernac_st) -let error loc msg vernac_st = Error ((loc,msg),(Some vernac_st)) +let error loc qf msg vernac_st = Error ((loc,msg), qf, (Some vernac_st)) type sentence_id = Stateid.t @@ -202,8 +202,9 @@ let interp_ast ~doc_id ~state_id ~st ~error_recovery ast = log @@ "Failed to execute: " ^ Stateid.to_string state_id ^ " " ^ (Pp.string_of_ppcmds @@ Ppvernac.pr_vernac ast); *) let loc = Loc.get_loc info in + let qf = Quickfix.get_qf info in let msg = CErrors.iprint (e, info) in - let status = error loc msg st in + let status = error loc qf msg st in let st = interp_error_recovery error_recovery st in st, status, [] @@ -521,11 +522,11 @@ let handle_event event state = | (Delegated (_,completion), fl), _ -> Option.default ignore completion v; Some (update_all id (Done v) fl state), Some id - | (Done (Success s), fl), Error (err,_) -> + | (Done (Success s), fl), Error (err,qf, _) -> (* This only happens when a Qed closing a delegated proof receives an updated by a worker saying that the proof is not completed *) - Some (update_all id (Done (Error (err,s))) fl state), Some id + Some (update_all id (Done (Error (err,qf,s))) fl state), Some id | (Done _, _), _ -> None, Some id | exception Not_found -> None, None (* TODO: is this possible? *) in @@ -577,14 +578,14 @@ let id_of_prepared_task = function let purge_state = function | Success _ -> Success None - | Error(e,_) -> Error (e,None) + | Error(e,_,_) -> Error (e,None,None) (* TODO move to proper place *) let worker_execute ~doc_id ~send_back (vs,events) = function | PSkip { id; error = err } -> let v = match err with | None -> success vs - | Some msg -> error None msg vs + | Some msg -> error None None msg vs in send_back (ProofJob.UpdateExecStatus (id,purge_state v)); (vs, events) @@ -612,8 +613,9 @@ let worker_ensure_proof_is_over vs send_back terminator_id = with e -> let e, info = Exninfo.capture e in let loc = Loc.get_loc info in + let qf = Quickfix.get_qf info in let msg = CErrors.iprint (e, info) in - let status = error loc msg vs in + let status = error loc qf msg vs in send_back (ProofJob.UpdateExecStatus (terminator_id,status)) let worker_main { ProofJob.tasks; initial_vernac_state = vs; doc_id; terminator_id } ~send_back = @@ -632,7 +634,7 @@ let worker_main { ProofJob.tasks; initial_vernac_state = vs; doc_id; terminator_ let execute st (vs, events, interrupted) task = if interrupted then begin - let st = update st (id_of_prepared_task task) (Error ((None,Pp.str "interrupted"),None)) in + let st = update st (id_of_prepared_task task) (Error ((None,Pp.str "interrupted"),None,None)) in (st, vs, events, true) end else try @@ -640,7 +642,7 @@ let execute st (vs, events, interrupted) task = | PSkip { id; error = err } -> let v = match err with | None -> success vs - | Some msg -> error None msg vs + | Some msg -> error None None msg vs in let st = update st id v in (st, vs, events, false) @@ -672,7 +674,7 @@ let execute st (vs, events, interrupted) task = assign (`Val (Declare.Proof.return_proof proof)) in Vernacstate.LemmaStack.with_top (Option.get @@ vernac_st.Vernacstate.interp.lemmas) ~f - | Error ((loc,err),_) -> + | Error ((loc,err),_,_) -> log "Aborted future"; assign (`Exn (CErrors.UserError err, Option.fold_left Loc.add_loc Exninfo.null loc)) with exn when CErrors.noncritical exn -> @@ -698,7 +700,7 @@ let execute st (vs, events, interrupted) task = (st, vs,events,false) end with Sys.Break -> - let st = update st (id_of_prepared_task task) (Error ((None,Pp.str "interrupted"),None)) in + let st = update st (id_of_prepared_task task) (Error ((None,Pp.str "interrupted"),None,None)) in (st, vs, events, true) let build_tasks_for document sch st id = @@ -708,7 +710,7 @@ let build_tasks_for document sch st id = (* We reached an already computed state *) log @@ "Reached computed state " ^ Stateid.to_string id; vs, tasks, st - | Some (Error(_,Some vs)) -> + | Some (Error(_,_,Some vs)) -> (* We try to be resilient to an error *) log @@ "Error resiliency on state " ^ Stateid.to_string id; vs, tasks, st @@ -737,13 +739,13 @@ let build_tasks_for document sch st id = let all_errors st = List.fold_left (fun acc (id, (p,_)) -> match p with - | Done (Error ((loc,e),_st)) -> (id,(loc,e)) :: acc + | Done (Error ((loc,e),qf,_)) -> (id,(loc,e,qf)) :: acc | _ -> acc) [] @@ SM.bindings st.of_sentence let error st id = match SM.find_opt id st.of_sentence with - | Some (Done (Error (err,_st)), _) -> Some err + | Some (Done (Error (err,_,_)), _) -> Some err | _ -> None let feedback st id = @@ -770,10 +772,10 @@ let shift_diagnostics_locs st ~start ~offset = in let shift_error (sentence_state, feedbacks as orig) = let sentence_state' = match sentence_state with - | Done (Error ((Some loc,e),st)) -> + | Done (Error ((Some loc,e),qf,st)) -> let loc' = shift_loc loc in if loc' == loc then sentence_state else - Done (Error ((Some loc',e),st)) + Done (Error ((Some loc',e),qf,st)) | _ -> sentence_state in let feedbacks' = CList.Smart.map shift_feedback feedbacks in @@ -790,12 +792,12 @@ let executed_ids st = let is_executed st id = match find_fulfilled_opt id st.of_sentence with - | Some (Success (Some _) | Error (_,Some _)) -> true + | Some (Success (Some _) | Error (_,_,Some _)) -> true | _ -> false let is_remotely_executed st id = match find_fulfilled_opt id st.of_sentence with - | Some (Success None | Error (_,None)) -> true + | Some (Success None | Error (_,_,None)) -> true | _ -> false let invalidate1 of_sentence id = @@ -862,10 +864,10 @@ let get_initial_context st = let get_vernac_state st id = match find_fulfilled_opt id st.of_sentence with | None -> log "Cannot find state for get_context"; None - | Some (Error (_,None)) -> log "State requested after error with no state"; None + | Some (Error (_,_,None)) -> log "State requested after error with no state"; None | Some (Success None) -> log "State requested in a remotely checked state"; None | Some (Success (Some st)) - | Some (Error (_, Some st)) -> + | Some (Error (_,_, Some st)) -> Some st module ProofWorkerProcess = struct diff --git a/language-server/dm/executionManager.mli b/language-server/dm/executionManager.mli index 1c3bf5e3..6be32d6e 100644 --- a/language-server/dm/executionManager.mli +++ b/language-server/dm/executionManager.mli @@ -51,7 +51,7 @@ val invalidate : Document.document -> Scheduler.schedule -> sentence_id -> state val error : state -> sentence_id -> (Loc.t option * Pp.t) option val feedback : state -> sentence_id -> feedback_message list -val all_errors : state -> (sentence_id * (Loc.t option * Pp.t)) list +val all_errors : state -> (sentence_id * (Loc.t option * Pp.t * Quickfix.t list option)) list val all_feedback : state -> (sentence_id * feedback_message) list val shift_diagnostics_locs : state -> start:int -> offset:int -> state From e0197022a66028c2cf35cdfc119c3c8bb1ffef2a Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Wed, 26 Jun 2024 11:21:56 +0200 Subject: [PATCH 7/8] Adapt to new API --- flake.lock | 2 +- language-server/dm/delegationManager.ml | 10 ++++---- language-server/dm/delegationManager.mli | 2 +- language-server/dm/document.ml | 18 +++++++------- language-server/dm/documentManager.ml | 21 +++++++++-------- language-server/dm/executionManager.ml | 30 ++++++++++++------------ language-server/dm/executionManager.mli | 2 +- language-server/dm/parTactic.ml | 2 +- language-server/protocol/lspWrapper.ml | 4 ++-- 9 files changed, 46 insertions(+), 45 deletions(-) diff --git a/flake.lock b/flake.lock index 107343a4..e94a7faa 100644 --- a/flake.lock +++ b/flake.lock @@ -16,7 +16,7 @@ "type": "github" }, "original": { - "owner": "gares", + "owner": "coq", "repo": "coq", "rev": "e139cf972cf2a876583ebbf5a19ffd419828116b", "type": "github" diff --git a/language-server/dm/delegationManager.ml b/language-server/dm/delegationManager.ml index 67e51360..ebe9f868 100644 --- a/language-server/dm/delegationManager.ml +++ b/language-server/dm/delegationManager.ml @@ -49,7 +49,7 @@ module type Job = sig val binary_name : string val initial_pool_size : int type update_request - val appendFeedback : Feedback.route_id * sentence_id -> (Feedback.level * Loc.t option * Pp.t) -> update_request + val appendFeedback : Feedback.route_id * sentence_id -> (Feedback.level * Loc.t option * Quickfix.t list * Pp.t) -> update_request end (* One typically created a job id way before the worker is spawned, so we @@ -66,8 +66,8 @@ let cancel_job (_,id) = keep here the conversion (STM) feedback -> (LSP) feedback *) let install_feedback send = - Log.feedback_add_feeder_on_Message (fun route span _ lvl loc _ msg -> - send (route,span,(lvl,loc,msg))) + Log.feedback_add_feeder_on_Message (fun route span _ lvl loc qf msg -> + send (route,span,(lvl,loc, qf, msg))) module type Worker = sig type job_t @@ -297,7 +297,7 @@ let handle_event = function exit 0 | Error(msg, cleanup_events) -> log @@ "worker did not spawn: " ^ msg; - (Some(Job.appendFeedback feedback_route (Feedback.Error,None,Pp.str msg)), cleanup_events) + (Some(Job.appendFeedback feedback_route (Feedback.Error,None,[],Pp.str msg)), cleanup_events) else match create_process_worker procname cancellation_handle job with | Ok events -> @@ -305,7 +305,7 @@ let handle_event = function (None, events) | Error(msg, cleanup_events) -> log @@ "worker did not spawn: " ^ msg; - (Some(Job.appendFeedback feedback_route (Feedback.Error,None,Pp.str msg)), cleanup_events) + (Some(Job.appendFeedback feedback_route (Feedback.Error,None,[],Pp.str msg)), cleanup_events) (* the only option is the socket port *) diff --git a/language-server/dm/delegationManager.mli b/language-server/dm/delegationManager.mli index 64c9b403..9b0856bb 100644 --- a/language-server/dm/delegationManager.mli +++ b/language-server/dm/delegationManager.mli @@ -42,7 +42,7 @@ module type Job = sig type update_request (** Called to handle feedback sent by the worker process *) - val appendFeedback : Feedback.route_id * sentence_id -> (Feedback.level * Loc.t option * Pp.t) -> update_request + val appendFeedback : Feedback.route_id * sentence_id -> (Feedback.level * Loc.t option * Quickfix.t list * Pp.t) -> update_request end type job_handle diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml index 7d342415..0dd9a931 100644 --- a/language-server/dm/document.ml +++ b/language-server/dm/document.ml @@ -330,7 +330,7 @@ let get_loc_from_info_or_exn e info = let get_loc_from_info_or_exn _ info = Loc.get_loc info -let get_qf_from_info info = Quickfix.get_qf info +(* let get_qf_from_info info = Quickfix.get_qf info *) [%%endif] [%%if coq = "8.18" || coq = "8.19"] @@ -381,25 +381,25 @@ let rec parse_more synterp_state stream raw parsed parsed_comments errors = with exn -> let e, info = Exninfo.capture exn in let loc = get_loc_from_info_or_exn e info in - let qf = get_qf_from_info info in - handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) qf + let qf = Result.value ~default:[] @@ Quickfix.from_exception e in + handle_parse_error start (loc, Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf) end | exception (E msg as exn) -> let loc = Loc.get_loc @@ Exninfo.info exn in - let qf = Quickfix.get_qf @@ Exninfo.info exn in + let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in junk_sentence_end stream; - handle_parse_error start (loc,msg) qf + handle_parse_error start (loc,msg) (Some qf) | exception (CLexer.Error.E e as exn) -> (* May be more problematic to handle for the diff *) let loc = Loc.get_loc @@ Exninfo.info exn in - let qf = Quickfix.get_qf @@ Exninfo.info exn in + let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in junk_sentence_end stream; - handle_parse_error start (loc,CLexer.Error.to_string e) qf + handle_parse_error start (loc,CLexer.Error.to_string e) (Some qf) | exception exn -> let e, info = Exninfo.capture exn in let loc = Loc.get_loc @@ info in - let qf = Quickfix.get_qf @@ Exninfo.info exn in + let qf = Result.value ~default:[] @@ Quickfix.from_exception exn in junk_sentence_end stream; - handle_parse_error start (loc, "Unexpected parse error: " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) qf + handle_parse_error start (loc, "Unexpected parse error: " ^ Pp.string_of_ppcmds @@ CErrors.iprint_no_report (e,info)) (Some qf) end let parse_more synterp_state stream raw = diff --git a/language-server/dm/documentManager.ml b/language-server/dm/documentManager.ml index 88741044..e6f127fa 100644 --- a/language-server/dm/documentManager.ml +++ b/language-server/dm/documentManager.ml @@ -127,15 +127,16 @@ let make_diagnostic doc range oloc message severity code = | Some (x,z) -> Some x, Some z in Diagnostic.create ?code ?data ~range ~message ~severity () -let mk_diag st (id,(lvl,oloc,msg)) = - let code = - match lvl with - | Feedback.Warning quickfixes -> +let mk_diag st (id,(lvl,oloc,qf,msg)) = + let code = + match qf with + | [] -> None + | qf -> let code : Jsonrpc.Id.t * Lsp.Import.Json.t = let open Lsp.Import.Json in (`String "quickfix-replace", - quickfixes |> yojson_of_list - (fun qf -> + qf |> yojson_of_list + (fun qf -> let s = Pp.string_of_ppcmds @@ Quickfix.pp qf in let loc = Quickfix.loc qf in let range = RawDocument.range_of_loc (Document.raw_document st.document) loc in @@ -143,9 +144,9 @@ let mk_diag st (id,(lvl,oloc,msg)) = )) in Some code - | _ -> None in - let lvl = DiagnosticSeverity.of_feedback_level lvl in - make_diagnostic st.document (Document.range_of_id st.document id) oloc (Pp.string_of_ppcmds msg) lvl code + in + let lvl = DiagnosticSeverity.of_feedback_level lvl in + make_diagnostic st.document (Document.range_of_id st.document id) oloc (Pp.string_of_ppcmds msg) lvl code let mk_error_diag st (id,(oloc,msg,qf)) = (* mk_diag st (id,(Feedback.Error,oloc, msg)) *) let code = @@ -222,7 +223,7 @@ let get_messages st pos = | Some id -> log "get_messages: Found id"; let error = ExecutionManager.error st.execution_state id in let feedback = ExecutionManager.feedback st.execution_state id in - let feedback = List.map (fun (lvl,_oloc,msg) -> DiagnosticSeverity.of_feedback_level lvl, pp_of_coqpp msg) feedback in + let feedback = List.map (fun (lvl,_oloc,_,msg) -> DiagnosticSeverity.of_feedback_level lvl, pp_of_coqpp msg) feedback in match error with | Some (_oloc,msg) -> (DiagnosticSeverity.Error, pp_of_coqpp msg) :: feedback | None -> feedback diff --git a/language-server/dm/executionManager.ml b/language-server/dm/executionManager.ml index 6f63e3bb..8222895b 100644 --- a/language-server/dm/executionManager.ml +++ b/language-server/dm/executionManager.ml @@ -19,6 +19,8 @@ open Types let Log log = Log.mk_log "executionManager" +type feedback_message = Feedback.level * Loc.t option * Quickfix.t list * Pp.t + type execution_status = | Success of Vernacstate.t option | Error of Pp.t Loc.located * Quickfix.t list option * Vernacstate.t option (* State to use for resiliency *) @@ -30,8 +32,6 @@ type sentence_id = Stateid.t module SM = Map.Make (Stateid) -type feedback_message = Feedback.level * Loc.t option * Pp.t - type sentence_state = | Done of execution_status | Delegated of DelegationManager.job_handle * (execution_status -> unit) option @@ -73,7 +73,7 @@ type state = { (* ugly stuff to correctly dispatch Coq feedback *) doc_id : document_id; (* unique number used to interface with Coq's Feedback *) coq_feeder : coq_feedback_listener; - sel_feedback_queue : (Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Pp.t)) Queue.t; + sel_feedback_queue : (Feedback.route_id * sentence_id * feedback_message) Queue.t; sel_cancellation_handle : Sel.Event.cancellation_handle; overview: exec_overview; } @@ -113,7 +113,7 @@ type prepared_task = module ProofJob = struct type update_request = | UpdateExecStatus of sentence_id * execution_status - | AppendFeedback of Feedback.route_id * Types.sentence_id * (Feedback.level * Loc.t option * Pp.t) + | AppendFeedback of Feedback.route_id * Types.sentence_id * (Feedback.level * Loc.t option * Quickfix.t list * Pp.t) let appendFeedback (rid,sid) fb = AppendFeedback(rid,sid,fb) type t = { @@ -131,7 +131,7 @@ end module ProofWorker = DelegationManager.MakeWorker(ProofJob) type event = - | LocalFeedback of (Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Pp.t)) Queue.t * Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Pp.t) + | LocalFeedback of (Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Quickfix.t list * Pp.t)) Queue.t * Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Quickfix.t list * Pp.t) | ProofWorkerEvent of ProofWorker.delegation type events = event Sel.Event.t list let pr_event = function @@ -202,9 +202,9 @@ let interp_ast ~doc_id ~state_id ~st ~error_recovery ast = log @@ "Failed to execute: " ^ Stateid.to_string state_id ^ " " ^ (Pp.string_of_ppcmds @@ Ppvernac.pr_vernac ast); *) let loc = Loc.get_loc info in - let qf = Quickfix.get_qf info in + let qf = Result.value ~default:[] @@ Quickfix.from_exception e in let msg = CErrors.iprint (e, info) in - let status = error loc qf msg st in + let status = error loc (Some qf) msg st in let st = interp_error_recovery error_recovery st in st, status, [] @@ -468,8 +468,8 @@ let local_feedback feedback_queue : event Sel.Event.t = Sel.On.queue ~name:"feedback" ~priority:PriorityManager.feedback feedback_queue (fun (rid,sid,msg) -> LocalFeedback(feedback_queue,rid,sid,msg)) let install_feedback_listener doc_id send = - Log.feedback_add_feeder_on_Message (fun route span doc lvl loc _ msg -> - if lvl != Feedback.Debug && doc = doc_id then send (route,span,(lvl,loc,msg))) + Log.feedback_add_feeder_on_Message (fun route span doc lvl loc qf msg -> + if lvl != Feedback.Debug && doc = doc_id then send (route,span,(lvl,loc, qf, msg))) let init vernac_state = let doc_id = fresh_doc_id () in @@ -497,8 +497,8 @@ let feedback_cleanup { coq_feeder; sel_feedback_queue; sel_cancellation_handle } let handle_feedback id fb state = match fb with - | (Feedback.Info, _, _) -> state - | (_, _, msg) -> + | (Feedback.Info, _, _, _) -> state + | (_, _, _, msg) -> begin match SM.find id state.of_sentence with | (s,fl) -> update_all id s (fb::fl) state | exception Not_found -> @@ -613,9 +613,9 @@ let worker_ensure_proof_is_over vs send_back terminator_id = with e -> let e, info = Exninfo.capture e in let loc = Loc.get_loc info in - let qf = Quickfix.get_qf info in + let qf = Result.value ~default:[] @@ Quickfix.from_exception e in let msg = CErrors.iprint (e, info) in - let status = error loc qf msg vs in + let status = error loc (Some qf) msg vs in send_back (ProofJob.UpdateExecStatus (terminator_id,status)) let worker_main { ProofJob.tasks; initial_vernac_state = vs; doc_id; terminator_id } ~send_back = @@ -763,12 +763,12 @@ let shift_diagnostics_locs st ~start ~offset = else if loc_stop > start then Loc.shift_loc 0 offset loc else loc in - let shift_feedback (level, oloc, msg as feedback) = + let shift_feedback (level, oloc, qf, msg as feedback) = match oloc with | None -> feedback | Some loc -> let loc' = shift_loc loc in - if loc' == loc then feedback else (level, Some loc', msg) + if loc' == loc then feedback else (level, Some loc', qf, msg) in let shift_error (sentence_state, feedbacks as orig) = let sentence_state' = match sentence_state with diff --git a/language-server/dm/executionManager.mli b/language-server/dm/executionManager.mli index 6be32d6e..67842673 100644 --- a/language-server/dm/executionManager.mli +++ b/language-server/dm/executionManager.mli @@ -37,7 +37,7 @@ type state type event type events = event Sel.Event.t list -type feedback_message = Feedback.level * Loc.t option * Pp.t +type feedback_message = Feedback.level * Loc.t option * Quickfix.t list * Pp.t val pr_event : event -> Pp.t diff --git a/language-server/dm/parTactic.ml b/language-server/dm/parTactic.ml index 169e62bc..8dbb0cf8 100644 --- a/language-server/dm/parTactic.ml +++ b/language-server/dm/parTactic.ml @@ -25,7 +25,7 @@ module TacticJob = struct | Error of Pp.t type update_request = | UpdateSolution of Evar.t * solution - | AppendFeedback of Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Pp.t) + | AppendFeedback of Feedback.route_id * sentence_id * (Feedback.level * Loc.t option * Quickfix.t list * Pp.t) let appendFeedback (rid,id) fb = AppendFeedback(rid,id,fb) type t = { diff --git a/language-server/protocol/lspWrapper.ml b/language-server/protocol/lspWrapper.ml index c15af6c3..d642f62d 100644 --- a/language-server/protocol/lspWrapper.ml +++ b/language-server/protocol/lspWrapper.ml @@ -79,7 +79,7 @@ module DiagnosticSeverity = struct let of_feedback_level = let open DiagnosticSeverity in function | Feedback.Error -> Error - | Feedback.Warning _ -> Warning + | Feedback.Warning -> Warning | Feedback.(Info | Debug | Notice) -> Information end @@ -101,7 +101,7 @@ module FeedbackChannel = struct | Feedback.Debug -> Some Debug | Feedback.Info -> Some Info | Feedback.Notice -> Some Notice - | Feedback.(Error | Warning _) -> None + | Feedback.(Error | Warning) -> None end From 7a118bebaf0f17198864104951ee1d1a1bff7f28 Mon Sep 17 00:00:00 2001 From: Romain Tetley Date: Thu, 11 Jul 2024 15:53:11 +0200 Subject: [PATCH 8/8] Create dummy quickfix type for coq 8.18 and 8.19 --- language-server/dm/types.ml | 9 +++++++++ language-server/protocol/lspWrapper.ml | 2 +- 2 files changed, 10 insertions(+), 1 deletion(-) diff --git a/language-server/dm/types.ml b/language-server/dm/types.ml index 616c3475..32bb2497 100644 --- a/language-server/dm/types.ml +++ b/language-server/dm/types.ml @@ -24,6 +24,15 @@ type exec_overview = { let empty_overview = {processing = []; processed = []; prepared = []} +[%%if coq = "8.18" || coq = "8.19"] + module Quickfix = struct + type t = unit + let from_exception _ = Ok([]) + let pp = Pp.mt + let loc _ = Loc.make_loc (0,0) + end +[%%endif] + type text_edit = Range.t * string type link = { diff --git a/language-server/protocol/lspWrapper.ml b/language-server/protocol/lspWrapper.ml index d642f62d..d35c09c4 100644 --- a/language-server/protocol/lspWrapper.ml +++ b/language-server/protocol/lspWrapper.ml @@ -3,7 +3,7 @@ (* VSCoq *) (* *) (* Copyright INRIA and contributors *) -(* (see version control and README file for authors & dates)Variables A : Type. *) +(* (see version control and README file for authors & dates) *) (* *) (**************************************************************************) (* *)