feat: add language server lsp API to get document proofs

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 =

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]. *)

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

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;
-    }
+    }
+
+let mk_proof_step tactic range = {tactic; range}
+
+let mk_proof_block statement steps range = {statement; steps; range}

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

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