From 3579e9d3d07b604ddc0aa480d2dab3ee2b376abb Mon Sep 17 00:00:00 2001
From: Romain Tetley <romain.tetley@inria.fr>
Date: Thu, 12 Dec 2024 15:51:39 +0100
Subject: [PATCH] feat: adding external api for running tactics at loc

---
 client/src/extension.ts        | 16 ++++++++++++++--
 client/src/protocol/types.ts   | 10 ++++++++++
 language-server/dm/document.ml |  2 +-
 3 files changed, 25 insertions(+), 3 deletions(-)

diff --git a/client/src/extension.ts b/client/src/extension.ts
index f60a0149f..bbb887b9d 100644
--- a/client/src/extension.ts
+++ b/client/src/extension.ts
@@ -9,7 +9,8 @@ import {workspace, window, commands, languages, ExtensionContext, env,
   extensions,
   StatusBarAlignment,
   MarkdownString,
-  WorkspaceEdit
+  WorkspaceEdit,
+  Position
 } from 'vscode';
 
 import {
@@ -27,6 +28,8 @@ import GoalPanel from './panels/GoalPanel';
 import SearchViewProvider from './panels/SearchViewProvider';
 import {
     CoqLogMessage,
+    CoqPilotRequest,
+    CoqPilotResponse,
     DocumentProofsRequest,
     DocumentProofsResponse,
     ErrorAlertNotification,
@@ -69,6 +72,14 @@ export function activate(context: ExtensionContext) {
         return client.sendRequest(req, params);
     };
 
+    const runTacticsAtLocContext = (uri: Uri, position: Position, text: string) => {
+        const textDocument = TextDocumentIdentifier.create(uri.toString());
+        const params: CoqPilotRequest = {textDocument, position, text};
+        const req = new RequestType<CoqPilotRequest, CoqPilotResponse, void>("vscoq/coqPilot");
+        Client.writeToVscoq2Channel("Trying running tactics: (" + text + ") for document: " + uri.toString());
+        return client.sendRequest(req, params);
+    };
+
     // Watch for files being added or removed
     workspace.onDidCreateFiles(checkInCoqProject);
     workspace.onDidDeleteFiles(checkInCoqProject);
@@ -381,7 +392,8 @@ Path: \`${coqTM.getVsCoqTopPath()}\`
     }
 
     const externalApi = {
-        getDocumentProofs
+        getDocumentProofs,
+        runTacticsAtLocContext
     };
 
     return externalApi;
diff --git a/client/src/protocol/types.ts b/client/src/protocol/types.ts
index c72a3e8a3..377439993 100644
--- a/client/src/protocol/types.ts
+++ b/client/src/protocol/types.ts
@@ -168,3 +168,13 @@ type ProofBlock = {
 export interface DocumentProofsResponse {
     proofs: ProofBlock[];
 }
+
+export interface CoqPilotRequest {
+    textDocument: TextDocumentIdentifier;
+    position: Position;
+    text: string;
+}
+
+export interface CoqPilotResponse {
+    errors: string[];
+}
diff --git a/language-server/dm/document.ml b/language-server/dm/document.ml
index f2a985c08..d713db4cb 100644
--- a/language-server/dm/document.ml
+++ b/language-server/dm/document.ml
@@ -545,7 +545,7 @@ let handle_parse_more ({loc; synterp_state; stream; raw; parsed; parsed_comments
           let str = String.sub (RawDocument.text raw) begin_char (end_char - begin_char) in
           let sstr = Stream.of_string str in
           let lex = CLexer.Lexer.tok_func sstr in
-          stream_tok 0 [] lex begin_line begin_char 
+          stream_tok 0 [] lex begin_line begin_char
         in
       begin
         try