Quickfix

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; */
+	}
+}

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(() => {
 

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"

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,15 +297,15 @@ 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 ->
           log "worker spawned (create_process)";
           (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 *)

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

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 = 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 = Result.value ~default:[] @@ Quickfix.from_exception exn in
       junk_sentence_end stream;
-      handle_parse_error start (loc,msg)
+      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 = Result.value ~default:[] @@ Quickfix.from_exception 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) (Some qf)
     | exception exn ->
       let e, info = Exninfo.capture exn in
       let loc = Loc.get_loc @@ info 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))
+      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 =

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

language-server/dm/documentManager.ml

@@ -114,28 +114,86 @@ 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,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",
+        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 lvl in
+    make_diagnostic st.document (Document.range_of_id st.document id) oloc (Pp.string_of_ppcmds msg) lvl code
 
-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
+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_error_diag st (id,(oloc,msg)) = mk_diag st (id,(Feedback.Error,oloc, msg))
 
-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
+  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
@@ -165,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