Skip to content

Commit

Permalink
Fix formatting
Browse files Browse the repository at this point in the history
  • Loading branch information
K-dizzled committed Dec 4, 2024
1 parent 7f634a2 commit 012fb42
Show file tree
Hide file tree
Showing 6 changed files with 57 additions and 30 deletions.
56 changes: 37 additions & 19 deletions src/coqLsp/coqLspClient.ts
Original file line number Diff line number Diff line change
Expand Up @@ -246,28 +246,46 @@ export class CoqLspClientImpl implements CoqLspClient {
}

trackSuspiciousLspErrors() {
this.client.onNotification(PublishDiagnosticsNotification.type, (params: PublishDiagnosticsParams) => {
function filterIncorrectLspSuspectedDiagnostics(diagnostic: Diagnostic): boolean {
const errorSubstrings = [
"Cannot find a physical path bound to logical path",
"Dynlink error: error loading shared library"
]

return errorSubstrings.some((substr) => diagnostic.message.includes(substr) && diagnostic.severity === 1);
}
this.client.onNotification(
PublishDiagnosticsNotification.type,
(params: PublishDiagnosticsParams) => {
function filterIncorrectLspSuspectedDiagnostics(
diagnostic: Diagnostic
): boolean {
const errorSubstrings = [
"Cannot find a physical path bound to logical path",
"Dynlink error: error loading shared library",
];

return errorSubstrings.some(
(substr) =>
diagnostic.message.includes(substr) &&
diagnostic.severity === 1
);
}

const suspectedDiagnostics = params.diagnostics.filter(filterIncorrectLspSuspectedDiagnostics);
if (suspectedDiagnostics.length > 0) {
const data = {
uri: params.uri.toString(),
version: params.version,
diagnosticMessage: suspectedDiagnostics.map((d) => d.message)
const suspectedDiagnostics = params.diagnostics.filter(
filterIncorrectLspSuspectedDiagnostics
);
if (suspectedDiagnostics.length > 0) {
const data = {
uri: params.uri.toString(),
version: params.version,
diagnosticMessage: suspectedDiagnostics.map(
(d) => d.message
),
};
const firstErrorMessage =
suspectedDiagnostics[0].message.split("\n")[0];

this.eventLogger?.log(
CoqLspConnector.wrongServerSuspectedEvent,
firstErrorMessage,
data
);
}
const firstErrorMessage = suspectedDiagnostics[0].message.split("\n")[0];

this.eventLogger?.log(CoqLspConnector.wrongServerSuspectedEvent, firstErrorMessage, data);
}
});
);
}

filterDiagnostics(
Expand Down
5 changes: 4 additions & 1 deletion src/coqLsp/coqLspConnector.ts
Original file line number Diff line number Diff line change
Expand Up @@ -79,7 +79,10 @@ export class CoqLspConnector extends LanguageClient {

override error(message: string, data: any, showNotification = true) {
if (this.isVersioningError(message)) {
this.eventLogger?.log(CoqLspConnector.wrongServerSuspectedEvent, message);
this.eventLogger?.log(
CoqLspConnector.wrongServerSuspectedEvent,
message
);
} else {
this.eventLogger?.log("coq-lsp-error", message);
}
Expand Down
9 changes: 6 additions & 3 deletions src/core/coqProofChecker.ts
Original file line number Diff line number Diff line change
Expand Up @@ -4,8 +4,8 @@ import { Position } from "vscode-languageclient";
import { CoqLspClient } from "../coqLsp/coqLspClient";
import { CoqLspTimeoutError } from "../coqLsp/coqLspTypes";

import { Uri } from "../utils/uri";
import { EventLogger } from "../logging/eventLogger";
import { Uri } from "../utils/uri";

export interface ProofCheckResult {
proof: string;
Expand All @@ -18,7 +18,10 @@ type Proof = string;
export class CoqProofChecker {
private mutex: Mutex = new Mutex();

constructor(private coqLspClient: CoqLspClient, private eventLogger?: EventLogger) {}
constructor(
private coqLspClient: CoqLspClient,
private eventLogger?: EventLogger
) {}

async checkProofs(
fileUri: Uri,
Expand Down Expand Up @@ -82,7 +85,7 @@ export class CoqProofChecker {

if (goalsResult.err) {
this.eventLogger?.log(
'new-proof-check',
"new-proof-check",
`Checking proog: ${proof}, goalsResult: ${goalsResult.val.message}`
);
}
Expand Down
5 changes: 1 addition & 4 deletions src/extension/coqPilot.ts
Original file line number Diff line number Diff line change
Expand Up @@ -335,10 +335,7 @@ export class CoqPilot {
}

private registerCommand(command: string, fn: () => void) {
let disposable = commands.registerCommand(
`${pluginId}.` + command,
fn
);
let disposable = commands.registerCommand(`${pluginId}.` + command, fn);
this.vscodeContext.subscriptions.push(disposable);
}

Expand Down
7 changes: 5 additions & 2 deletions src/extension/sessionState.ts
Original file line number Diff line number Diff line change
Expand Up @@ -2,15 +2,18 @@ import { Disposable, OutputChannel } from "vscode";

import { createCoqLspClient } from "../coqLsp/coqLspBuilders";
import { CoqLspClient } from "../coqLsp/coqLspClient";
import { CoqLspConnector } from "../coqLsp/coqLspConnector";

import { CompletionAbortError } from "../core/abortUtils";

import { EventLogger, Severity } from "../logging/eventLogger";

import { parseCoqLspServerPath } from "./settings/configReaders";
import {
EditorMessages,
showMessageToUser,
} from "./ui/messages/editorMessages";
import { PluginStatusIndicator } from "./ui/pluginStatusIndicator";
import { CoqLspConnector } from "../coqLsp/coqLspConnector";
import { EditorMessages, showMessageToUser } from "./ui/messages/editorMessages";

export class SessionState implements Disposable {
private _isActive = true;
Expand Down
5 changes: 4 additions & 1 deletion src/extension/ui/messages/editorMessages.ts
Original file line number Diff line number Diff line change
Expand Up @@ -36,7 +36,10 @@ export namespace EditorMessages {
export const extensionIsPaused =
"You have stopped CoqPilot. To resume, click on the CoqPilot icon in the status bar.";

export const wrongCoqLspSuspected = (coqLspPath: string, errorMessage: string): string =>
export const wrongCoqLspSuspected = (
coqLspPath: string,
errorMessage: string
): string =>
`CoqPilot suspects that the Coq-LSP server located at ${coqLspPath} is not working as expected, error received from server: \"${errorMessage}\". Please make sure that the server is properly installed and the path to it is set correctly in the settings.`;

export const objectWasThrownAsError = (e: any) =>
Expand Down

0 comments on commit 012fb42

Please sign in to comment.