Skip to content

Commit

Permalink
Change the way lsp server is launched from Vscode extension (#1164)
Browse files Browse the repository at this point in the history
As described in issue #1163 , one may want to launch the `Lambdapi Lsp server` from the `Vscode` extension  using a custom command. This is especially useful when installing the `Lambdapi extension` on `Windows` where `Lambdapi` is launched through `wsl`. This is done in this PR by allowing to read the arguments of the launch command as well as the command it self, from the `package.json` file instead of wiring it in the code.
  • Loading branch information
Alidra authored Dec 19, 2024
1 parent 35a5beb commit ad4666d
Show file tree
Hide file tree
Showing 4 changed files with 28 additions and 9 deletions.
9 changes: 9 additions & 0 deletions editors/vscode/CHANGES.md
Original file line number Diff line number Diff line change
Expand Up @@ -3,6 +3,15 @@ All notable changes to this project will be documented in this file.
The format is based on [Keep a Changelog](https://keepachangelog.com/),
and this project adheres to [Semantic Versioning](https://semver.org/).

## Unreleased

### Added

### Fixed

### Changed
- When calling lambdapi to launch the lsp server from the Vscode extension, read the `lsp` argument from `package.json` instead of hard-coding it to allow using a custom command to launch the server especially in Windows as discussed in issue #1163 (Many thanks to Akihisa Yamada)

## [0.2.2]
- code refactoring of the client for maintenability.
- fix the bug that causes the proof navigation to malfunction when the `Goals` panel is closed by the user. Now the panel is recreated whenever needed. If focus is taken away frol the `Goals` panel, focus is given back to it when user starts navigating proofs again.
Expand Down
11 changes: 9 additions & 2 deletions editors/vscode/package.json
Original file line number Diff line number Diff line change
Expand Up @@ -58,7 +58,14 @@
"lambdapi.path": {
"type": "string",
"default": "lambdapi",
"description": "Path to lambdapi binary"
"description": "Command to launch lambdapi"
},
"lambdapi.args": {
"type": "list",
"default": [
"lsp"
],
"description": "Arguments to start the Lsp server"
}
}
},
Expand Down Expand Up @@ -170,4 +177,4 @@
"fs-extra": "^9.0.1",
"vscode-languageclient": "^9.0.1"
}
}
}
6 changes: 3 additions & 3 deletions editors/vscode/src/browser.ts
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,10 @@ import { LanguageClient } from "vscode-languageclient/node";
import { activateClientLSP, ClientFactoryType, deactivateClientLSP } from "./client";

export function activate(context: ExtensionContext): void {
const cf: ClientFactoryType = (context, clientOptions, wsConfig, lspServerPath) => {
const cf: ClientFactoryType = (context, clientOptions, wsConfig, lpLaunchCommand, lspLaunchArgs) => {
let serverOptions = {
command: lspServerPath,
args: ['lsp']
command: lpLaunchCommand,
args: lspLaunchArgs
};
return new LanguageClient(
"lambdapi",
Expand Down
11 changes: 7 additions & 4 deletions editors/vscode/src/client.ts
Original file line number Diff line number Diff line change
Expand Up @@ -62,7 +62,8 @@ export type ClientFactoryType = (
context: ExtensionContext,
clientOptions: LanguageClientOptions,
wsConfig: WorkspaceConfiguration,
lspServerPath: any,
lpLaunchCommand: any,
lspServerArgs: any,
) => BaseLanguageClient;

// The implementation of the VSCode lambdapi extension commands.
Expand Down Expand Up @@ -354,8 +355,10 @@ export function activateClientLSP(context: ExtensionContext,
//Following mode : whether the window follows proofState automatically or not
context.workspaceState.update('follow', true);

const lspServerPath = workspace.getConfiguration('lambdapi').path;
console.log(lspServerPath);
const lpLaunchCommand = workspace.getConfiguration('lambdapi').path;
const lspLaunchArgs = workspace.getConfiguration('lambdapi').args;
console.log(lpLaunchCommand);
console.log(lspLaunchArgs);

const wsConfig = workspace.getConfiguration("lambdapi");

Expand All @@ -380,7 +383,7 @@ export function activateClientLSP(context: ExtensionContext,

let cP = new Promise<BaseLanguageClient>((resolve) => {
// Create a client using the factory
client = clientFactory(context, clientOptions, wsConfig, lspServerPath);
client = clientFactory(context, clientOptions, wsConfig, lpLaunchCommand, lspLaunchArgs);
resolve(client);
});

Expand Down

0 comments on commit ad4666d

Please sign in to comment.