feat: add a get document proofs external api

Now extensions that depend on vscoq can get all the document proofs.

client/src/client.ts

@@ -4,7 +4,6 @@ import {
   LanguageClient,
   LanguageClientOptions,
   ServerOptions,
-  integer
 } from 'vscode-languageclient/node';
 
 import {decorationsManual, decorationsContinuous, decorationsErrorAnimation} from './Decorations';

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

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[];
+}