From 0b05cfbd84d790d7c39c10daaadedd5dace0e66a Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Mon, 9 Dec 2024 11:26:45 +0100
Subject: [PATCH] feat: add a get document proofs external api

Now extensions that depend on vscoq can get all the document proofs.
---
 client/src/client.ts         |  1 -
 client/src/extension.ts      | 26 +++++++++++++++++++++++++-
 client/src/protocol/types.ts | 19 +++++++++++++++++++
 3 files changed, 44 insertions(+), 2 deletions(-)

diff --git a/client/src/client.ts b/client/src/client.ts
index b2a88826f..091be35c2 100644
--- a/client/src/client.ts
+++ b/client/src/client.ts
@@ -4,7 +4,6 @@ import {
   LanguageClient,
   LanguageClientOptions,
   ServerOptions,
-  integer
 } from 'vscode-languageclient/node';
 
 import {decorationsManual, decorationsContinuous, decorationsErrorAnimation} from './Decorations';
diff --git a/client/src/extension.ts b/client/src/extension.ts
index 138ba9a7c..8d4e64c68 100644
--- a/client/src/extension.ts
+++ b/client/src/extension.ts
@@ -27,6 +27,8 @@ import GoalPanel from './panels/GoalPanel';
 import SearchViewProvider from './panels/SearchViewProvider';
 import {
     CoqLogMessage,
+    DocumentProofsRequest,
+    DocumentProofsResponse,
     ErrorAlertNotification,
     MoveCursorNotification, 
     ProofViewNotification, 
@@ -186,6 +188,22 @@ export function activate(context: ExtensionContext) {
             });
         };
 
+        const getDocumentProofs = (editor: TextEditor) => {
+            const uri = editor.document.uri;
+            const textDocument = TextDocumentIdentifier.create(uri.toString());
+            const params: DocumentProofsRequest = {textDocument};
+            const req = new RequestType<DocumentProofsRequest, DocumentProofsResponse, void>("vscoq/documentProofs");
+            Client.writeToVscoq2Channel("Getting proofs for: " + uri.toString());
+            client.sendRequest(req, params).then(
+                (res) => {
+                    return res;
+                }, 
+                (err) => {
+                    window.showErrorMessage(err);
+                }
+            );
+        };
+
         registerVscoqTextCommand('reset', (editor) => {
             const uri = editor.document.uri;
             const textDocument = TextDocumentIdentifier.create(uri.toString());
@@ -368,7 +386,13 @@ Path: \`${coqTM.getVsCoqTopPath()}\`
         });
 
         context.subscriptions.push(client);
-    }	
+
+        const externalApi = {
+            getDocumentProofs
+        };
+
+        return externalApi;
+    }
 
 }
 
diff --git a/client/src/protocol/types.ts b/client/src/protocol/types.ts
index b8ae64c1e..74b555f59 100644
--- a/client/src/protocol/types.ts
+++ b/client/src/protocol/types.ts
@@ -144,3 +144,22 @@ export interface ResetCoqRequest {
 }
 
 export interface ResetCoqResponse {};
+
+export interface DocumentProofsRequest {
+    textDocument: TextDocumentIdentifier;
+}
+
+type proof_step = {
+    range: Range;
+    tactic: string;
+};
+
+type proof_block = {
+    statement: string;
+    range: Range;
+    proofs: proof_step[];
+};
+
+export interface DocumentProofsResponse {
+    proofs: proof_block[];
+}