Skip to content

Commit

Permalink
Add user warning when file was not saved before completion
Browse files Browse the repository at this point in the history
K-dizzled committed Aug 27, 2024

Verified

This commit was signed with the committer’s verified signature.
dwilkie David Wilkie
1 parent d09d094 commit 71846ce
Showing 3 changed files with 13 additions and 1 deletion.
2 changes: 1 addition & 1 deletion package.json
Original file line number Diff line number Diff line change
@@ -1,7 +1,7 @@
{
"name": "coqpilot",
"displayName": "СoqPilot",
"description": "An ai based completion extension for Coq interactive prover.",
"description": "An AI-based completion extension for Coq interactive prover.",
"icon": "etc/img/logo.ico",
"repository": {
"type": "git",
9 changes: 9 additions & 0 deletions src/extension/coqPilot.ts
Original file line number Diff line number Diff line change
@@ -148,6 +148,15 @@ export class CoqPilot {
"completion-started",
"CoqPilot has started the completion process"
);

if (editor.document.isDirty) {
showMessageToUser(
EditorMessages.saveFileBeforeCompletion,
"warning"
);
return;
}

const [completionContexts, sourceFileEnvironment, processEnvironment] =
await this.prepareForCompletions(
shouldCompleteHole,
3 changes: 3 additions & 0 deletions src/extension/editorMessages.ts
Original file line number Diff line number Diff line change
@@ -17,6 +17,9 @@ export namespace EditorMessages {
export const noProofsForAdmit = (lineWithAdmitNumber: number) =>
`CoqPilot failed to find a proof for the admit at line ${lineWithAdmitNumber}.`;

export const saveFileBeforeCompletion =
"Please note that this file has not been saved after the updates. Currently CoqPilot requires the file to be saved before the completion.";

export const noAdmitsFound =
"No admits were found in this selection/file. Make sure your coq-lsp is running correctly.";

0 comments on commit 71846ce

Please sign in to comment.