Skip to content

Commit

Permalink
vscode : do nothing when goals are null, get focus back for goals pan…
Browse files Browse the repository at this point in the history
…el before showing logs and goals
  • Loading branch information
Alidra committed Apr 17, 2024
1 parent 9a24661 commit 85355b7
Showing 1 changed file with 9 additions and 0 deletions.
9 changes: 9 additions & 0 deletions editors/vscode/src/client.ts
Original file line number Diff line number Diff line change
Expand Up @@ -664,6 +664,15 @@ function sendGoalsRequest(position: Position, panel: WebviewPanel, docUri: Uri,
let cursor = { textDocument: doc, position: position };
const req = new RequestType<ParamsGoals, GoalResp, void>("proof/goals");
client.sendRequest(req, cursor).then((goals) => {
// If uri is not a lambdapi/dedukti file, do nothing
if(goals.goals == null){
return;
}
// Take focus back if the goal panel lost it.
window.showErrorMessage("Going through Goals");
if(!panel.active) {
panel.reveal(2, false);
}

updateTerminalText(goals.logs);

Expand Down

0 comments on commit 85355b7

Please sign in to comment.