Adapt to new API

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

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

language-server/dm/documentManager.ml

@@ -127,25 +127,26 @@ 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
             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 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

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
@@ -191,9 +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 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, []
 
@@ -457,8 +457,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
@@ -486,8 +486,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 -> 
@@ -602,9 +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 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 =
@@ -752,12 +752,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

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
 

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

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