feat: adding external api for running tactics at loc

coq · Dec 13, 2024 · 5448664 · 5448664
1 parent f65b02b
commit 5448664
Show file tree

Hide file tree

Showing 3 changed files with 25 additions and 3 deletions.
diff --git 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
@@ -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
@@ -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