[language-server] Add support for quickfixes in errors

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 =

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

@@ -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

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
 
@@ -191,8 +191,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, []
 
@@ -510,11 +511,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
@@ -566,14 +567,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)
@@ -601,8 +602,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 =
@@ -621,15 +623,15 @@ 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
       match task with
       | 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)
@@ -661,7 +663,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 ->
@@ -687,7 +689,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 =
@@ -697,7 +699,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
@@ -726,13 +728,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 =
@@ -759,10 +761,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
@@ -779,12 +781,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 =
@@ -851,10 +853,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

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